Sémantique & application à la vérification

In this lecture, we will study techniques for reasoning about programs, so as to verify correctness properties. We will first set up the foundations of the semantics of programming languages and the notion of program proofs, using Hoare triples. Then, we will formalize various kind of relevant properties (safety, liveness, security). Last, we will focus on approaches for automatic program verification (abstract interpretation based static analysis, model checking of finite systems, solving modulo theory): the inference of the proofs is then performed by another computer program.

– Xavier Rival on his website


The project is available !

Practical session

The lab session base code is available in the moodle.

Please read the installation procedure and the syntax description

A correction is available on ENS gitlab.