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 2021-2022.

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: background on automated deduction, classical Hoare logic, partial correctness, weakest liberal preconditions, simple examples with Why3 and SMT solvers.
  • Slides: original or 4 per page
  • Examples of purely logic goals: propositional logic, first-order logic, equality, integer arithmetic
  • Simple basic contracts
  • Square root in Why3: ISQRT and its full solution
  • Canvas for exercises: Exercise 1, Exercise 2, Exercise 3
• Lecture 2 (December 4th): More advanced topics in program verification
  • Covers: a ML-style language, blocking semantics, treatment of local variables, labels, function calls and modularity aspects, specification languages, axiomatic specifications, product types, programs on arrays.
  • Slides: original or 4 per page
  • Solutions to exercices of lecture 1: Naive Sum , Euclidean division
  • Illustrative examples using Why3: Euclide's algorithm for GCD with labels, Euclidean division with local variable (can be executed on tests, see inside the file), Incrementation of a section of an array
  • Home work:
    • Search in an array : the linear version and then the binary version
• Lecture 3 (January 4th): Termination, Ghost code, More data structures, Exceptions, Computer Arithmetic
  • Covers: termination, ghost code, lemma functions, 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: Linear search,
  • Examples in Why3 or C from the slides: Euclid's remainder with ghost code, Factorial function, A Lemma function List reversal: Canvas and Solution, Exact square root, with an exception, Linear search with an exception: canvas and solution, Examples of overflow and rounding errors
  • Home Work:
    • Search in an array : the binary version and Linear version with a for loop
    • Termination of McCarthy's 91 function
    • Bézout coefficients using ghost code
    • Lemmas on power function, using lemma functions
    • Prove Fermat's little theorem for p=3
    • Binary search with an exception
• Lecture 4 (January 11th): 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:
    • McCarthy's 91 function
    • Lemmas on power function, using lemma functions
    • Binary search
    • Binary search with an exception
  • Examples in Why3: Stack part 1, Stack part 2, In place linked-list reversal canvas and complete solution
  • Optional home work In-place linked-list concatenation

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

• Lecture 5 (January 18th): Separation Logic 1
  • Covers: basic heap predicates, mutable lists, list segments, trees, sharing, specification triples.
  • slides, exercise sheet
• Lecture 6 (January 25th): Separation Logic 2
  • Covers: frame rule, heap entailment, structural rules, reasoning rules for terms, reasoning about functions.
  • slides, exercise sheet
• Lecture 7 (February 1st): Separation Logic 3
  • Covers: reasoning about loops, about aliasing, about local state, specification of higher-order functions, in particular iterators, characteristic formulas.
  • slides, exercise sheet
• Lecture 8 (February 8th): Separation Logic 4
  • Covers: higher-order representation predicates, resource analysis, complexity analysis, fractional and read-only permissions, parallelism, lock invariants, ghost variables and state.
  • slides, exercise sheet

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.

You may have a look at the exam of 2019-2020. 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 2020-2021. Once you have solved all exercises (and not before!), you may check some of the solutions.

• Course given in 2020-2021 (similar content)
• Course given in 2019-2020 (similar content)
• 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)