MPRI Course 2-36-1: Proof of Program
This page presents teaching material for Course 2-36-1 "Proof of Program" of the MPRI 2016-2017.
- Location: bâtiment Sophie Germain, room 2036.
- Time: Wednesday, 16:00 to 19:00.
- First course: December 7th.
- Project description: end of December.
- Project due: TBA (around mid February).
- Exam: either March 1st or March 8th.
Example programs for some lectures will be using the verification
environment Why3. There is an on-line version of Why3 that can be
used to replay the simplest examples. However, for more complex
examples and for the project that require several provers, it is
necessary to install Why3 and the automated provers.
You may find detailed instructions in this installation procedure.
Remark: there will be no course on January 4th.
The project was provided on January 10th.
The project consists of the formalization of several algorithms for answering range sum queries. Here is the skeleton file provided.
To install Why3 and the automated provers, follow the
Slides and examples will be posted here.
Part 1: Program verification using Hoare Logic, lectured by Claude Marché.
- Lecture 1 (December 7th): Basics of deductive program verification.
- Covers: classical Hoare logic, partial correctness, weakest liberal preconditions, blocking semantics, simple examples with Why3 and SMT solvers.
- Running example in Why3: ISQRT
- Canvas for exercises: Exercise 1, Exercise 2, Exercise 3
- Lecture 2 (December 14th): More advanced topics in program verification
- Covers: treatment of local variables, ghost variables and labels, function calls and modularity aspects, termination, specification languages, axiomatic specifications, lemma functions, programs on arrays.
- Solutions to exercices of lecture 1: Euclidean division, Fast exponentiation (hint to prove lemmas: increase Alt-Ergo' time limit to 60 seconds)
- Examples in Why3:
Euclid's algorithm for GCD with ghost variables,
Euclid's algorithm for GCD with labels,
Factorial computed with a while loop,
- Home work:
McCarthy's 91 function,
Search in an array : linear version
Prove Fermat's little theorem for p=3
No lecture on January 4th
- Lecture 3 (January 11th): More data structures, Exceptions, Computer Arithmetic
- Covers: products and sum types, lists ; handling exceptions ; computer arithmetic : machine integers, floating-point numbers.
- Solutions to home work from lecture 2:
McCarthy 91 function,
Lemma functions, little Fermat's theorem for n=3,
Linear search with a for loop,
- Examples in Why3 or C from the slides:
Exact square root, with an exception,
Examples of overflow and rounding errors,
Binary search using machine integers, why3 version,
Binary search in C,
"Clock drift", bounding rounding errors on successive additions of 0.1 ,
- Home Work:
Linear search with an exception,
Binary search with an exception,
- Lecture 4 (January 18th): Aliasing issues
- Covers: call by reference, alias control by static typing ; component-as-array modeling for pointer programs.
Part 2: Separation Logic and representation predicates, lectured by Arthur Charguéraud.
- Lecture 5 : Separation Logic 1
- Covers: basic heap predicates, mutable lists and trees, specification triples, list segments, frame rule.
- Lecture 6 : Separation Logic 2
- Covers: trees with invariants, arrays, structures with sharing, heap entailment, interpretation of triples, reasoning rules.
- Lecture 7 : Separation Logic 3
- Covers: specification of higher-order functions, higher-order representation predicates for specifying advanced data structures, and ownership transfer.
- Lecture 8 : Separation Logic 4
- Covers: higher-order representation predicates: arrays and iterations; Separation Logic in the Coq proof assistant; extensions of Separation Logic for parallelism and concurrency.
You may have a look at the exam of 2014.
Once you have solved all exercises (and not before!), you may check some of the solutions.
You may have a look at the exam of 2015. Once you have solved all exercises (and not before!), you may check some of the solutions.
You may have a look at the exam of 2016. Once you have solved all exercises (and not before!), you may check some of the solutions.
Page generated on 2017/1/12