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.

The page for year 2017-2018 is here

Organisation

Lectures

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.
  • Slides
  • 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.
  • Slides
  • 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, Lemma functions
  • Home work: Bézout coefficients, McCarthy's 91 function, Search in an array : linear version binary 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.
  • Slides
  • Solutions to home work from lecture 2: Bezout coefficient, McCarthy 91 function, Lemma functions, little Fermat's theorem for n=3, Linear search, Binary search, Linear search with a for loop,
  • Examples in Why3 or C from the slides: List reversal, 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.
  • Slides
  • Solutions to exercices of lecture 3: Linear search with an exception, Binary search with an exception,
  • Examples in Why3: Stack part 1, Stack part 2, In place linked-list reversal
  • Home work In-place linked-list concatenation

Part 2: Separation Logic and representation predicates, lectured by Arthur Charguéraud.

• All lectures, for printing:
  • Slides of all parts and printable version.
• Lecture 5 (January 25th): Separation Logic 1
  • Covers: basic heap predicates, mutable lists, list segments, trees, sharing, specification triples.
  • Slides of introduction
  • Slides of Part 1 and printable version.
• February 1st, Lab session, help with the project, same room as usual, bring your laptop
• Lecture 6 (February 8th): Separation Logic 2
  • Covers: frame rule, heap entailment, structural rules, reasoning rules for terms, reasoning about functions.
  • Slides of Part 2 and printable version.
• Lecture 7 (February 15th): Separation Logic 3
  • Covers: reasoning about loops, about aliasing, about local state, specification of higher-order functions, in particular iterators, and presentation of the basics characteristic formulae for conducting Separation Logic in the Coq proof assistant.
  • Slides of Part 3 and printable version.
• Lecture 8 (February 22th): Separation Logic 4
  • Covers: characteristic formulae (continued), higher-order representation predicates for describing containers that own their elements, and extensions of Separation Logic for parallelism and for amortized complexity analysis.
  • Slides of Part 4 and printable version.
• All lectures, for printing: see above.

Previous exams

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.

Past versions

• Course given in 2015-2016 (similar content)
• Course given in 2014-2015 (similar content)
• Course given in 2013-2014 (similar content)
• Course given in 2012-2013 (different content)
• Course given in 2011-2012 (different content)