- title:
- Proofs of Programs
Preuves de programmes - manager:
- Jean-Marie Madiot
- ects:
- 3
- period:
- 2
- hours:
- 24
- weeks:
- 8
- hours-per-week:
- 3
- language:
- English on request
- lang:
- track:
- B
- themes:
- Logic/Proof, Semantic/Languages, Verification
- order:
- 2.36.1
- successor:
- progproofs
- link:
- view
- [2.36.1]
- Proofs of Programs
Preuves de programmes
- Language:
- Period:
- 2.
- Duration:
- 24h (3h/week).
- ECTS:
- 3.
- Manager:
- Jean-Marie Madiot.
Teachers for 2024-2025: François Bobot, Jean-Marie Madiot
Lessons will be given in French by default, in English upon request. The slides and the lecture notes will be in English. In the past 4 years, the course has been taught in English.
Dates and files associated with the course are posted on the webpage of the course https://marche.gitlabpages.inria.fr/lecture-deductive-verif/
Objectives of the Course
Introduction to the various concepts and formalisms towards the proof that a program respects a given formal specification.
Outline
- Basics of deductive program verification:
- classical Hoare logic, partial/total correctness, weakest liberal preconditions, examples with Why3 and SMT solvers.
- More advanced topics in program verification:
- treatment of local variables, effects, exceptions, blocking semantics, modularity aspects.
- Handling of data structures:
- specification using abstract functions, sets, maps, and multi-sets; program on arrays; handling of machine integers and floating-point numbers.
- Aliasing issues:
- call by reference, alias control by static typing.
- Separation Logic Part 1:
- basic heap predicates, mutable lists and trees, specification triples, list segments, frame rule.
- Separation Logic Part 2:
- trees with invariants, arrays, structures with sharing, heap entailment, interpretation of triples, reasoning rules.
- Separation Logic Part 3:
- specification of higher-order functions, higher-order representation predicates for specifying advanced data structures, and ownership transfer.
- Separation Logic Part 4:
- higher-order representation predicates: arrays and iterations; Separation Logic in the Coq proof assistant; extensions of Separation Logic for parallelism and concurrency.
Pre-requisites
Basic knowledge on:
- syntax and semantics of first-order logic,
- formal deduction rules,
- operational semantics of programs.
Evaluation
Students will evaluated by a practical project and a final exam.
The final grade will be computed as : Max( (2/3 exam + 1/3 project), (3/4 exam + 1/4 project) ).