Logic-Based Analysis of Computation
The aim of the project “Logic-Based Analysis of Computation” is to develop logical tools for analysing and proving the correctness of programs. Ensuring the reliability of programs has become in the past two decades one of the main challenges of computer science. This is mainly due to the fact that computer programs are now at the heart of numerous systems where security is essential, as for example in transports. Since programming languages have been designed, formalisms and tools have been thought and developed to express and prove properties of programs. The majority of them rely on the semantics of syntactical constructions of programs.
This project links together two specific schools in the analysis of programs: The semantic tradition, represented by the French members, stressing that all formalism and tools that have been thought and developed to express and prove properties of programs rely on semantics of syntactical constructions of programs. And on the other hand the syntactic approach, stemming from rewriting and automated reasoning, as represented by the Austrian members. The latter approach is trying to exploit the structural properties of the formalism and relies in its proof methods on pure equational reasoning.
Members
- Georg Moser
- Michel Parigot
- ...