MPRI

MPRI Course 2-36-1: Proof of Program

• Home
• Organisation
• Tools
• Project
• Lectures
• Past years

This page presents teaching material for Course 2-36-1 "Proof of Program" of the MPRI 2019-2020.

Organisation

Lectures

Slides and examples will be posted here.

Part 1: Program verification using Hoare Logic, lectured by Claude Marché.

• Lecture 1 (December 3rd): Basics of deductive program verification.
  • Covers: background on automated deduction, classical Hoare logic, partial correctness, weakest liberal preconditions, blocking semantics, simple examples with Why3 and SMT solvers.
  • Slides: original or 4 per page
  • Examples of purely logic goals: propositional logic, first-order logic, integer arithmetic
  • Simple basic contracts
  • Square root in Why3: ISQRT
  • Canvas for exercises: Exercise 1, Exercise 2, Exercise 3
• No lecture on December 10th, due to the strike and transportation problems
• Lecture 2 (December 17th): More advanced topics in program verification
  • Covers: treatment of local variables, labels, function calls and modularity aspects, termination, specification languages, axiomatic specifications, product types, ghost code, lemma functions, programs on arrays.
  • Slides: original or 4 per page
  • Solutions to exercices of lecture 1: Inefficient sum, 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 labels, Euclid's remainder with ghost code, Lemma function
  • Home work: McCarthy's 91 function, Bézout coefficients, Factorial computed with a while loop, Search in an array : linear version binary version
• Lecture 3 (January 7th): More data structures, Exceptions, Computer Arithmetic
  • Covers: sum types, lists ; handling exceptions ; computer arithmetic : machine integers, floating-point numbers.
  • Slides: original or 4 per page
  • Solutions to home work from lecture 2: McCarthy 91 function, Bezout coefficient, Factorial function, Lemmas on power function, using lemma functions, Linear search
  • Examples in Why3 or C from the slides: List reversal, Exact square root, with an exception, Linear search with an exception, Examples of overflow and rounding errors, Binary search in C, "Clock drift", bounding rounding errors on successive additions of 0.1 ,
  • Home Work: little Fermat's theorem for n=3, Linear search with a for loop, Binary search, Binary search with an exception, Binary search using machine integers
• Lecture 4 (January 14th): Aliasing issues
  • Covers: call by reference, alias control by static typing ; component-as-array modeling for pointer programs.
  • Slides: original or 4 per page
  • Solutions to exercices of lecture 3: little Fermat's theorem for n=3, Linear search with a for loop, Binary search, Binary search with an exception, Binary search using machine integers
  • Examples in Why3: Stack part 1, Stack part 2, In place linked-list reversal
  • Home work In-place linked-list concatenation

Intermission: February 4th, Lab session, help with the project, same room as usual, bring your laptop

Part 2: Separation Logic and representation predicates, lectured by Jean-Marie Madiot. Ask Jean-Marie by email or in person if you'd like printable versions. Please note that the slides are subject to occasional change.

• Lecture 5 (January 21th): Separation Logic 1
  • Covers: basic heap predicates, mutable lists, list segments, trees, sharing, specification triples.
  • Slides of introduction
  • Slides of lecture 1
  • Exercises sheet used during the session (not useful by itself)
  • Interactive proofs: online or installation instructions.
• Lecture 6 (January 28th): Separation Logic 2
  • Covers: frame rule, heap entailment, structural rules, reasoning rules for terms, reasoning about functions.
  • Slides of lecture 2
  • Exercises sheet used during the session (not useful by itself)
• Lab session (February 4th)
• Lecture 7 (February 11th): 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 lecture 3
  • Exercises sheet used during the session (not useful by itself)
• Lecture 8 (February 18th): 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 lecture 4
  • Exercises sheet used during the session (not useful by itself)

Past Years

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.

You may have a look at the exam of 2017. Once you have solved all exercises (and not before!), you may check some of the solutions.

• Course given in 2018-2019 (similar content)
• Course given in 2017-2018 (similar content)
• Course given in 2016-2017 (similar content)
• 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)