MPRI Course 2-36-1: Proof of Program
This page presents teaching material for the Lecture 2-36-1 "proof of program" of the MPRI.
See also the page for year 2011-2012
- Return date for the project: Monday, March 11th, 12:00 UTC
Variations around the Sudoku Puzzle, and the grid.mlw file
- Final exam: March 6th, 16:15 - 19:15
location: usual lecture room (room 1008, Sophie Germain)
allowed documents: lecture notes, personal notes but no electronic device
(tentative schedule, subject to changes)
- Lecture 1 (December 12th): Classical Hoare Logic, Partial
correctness, Weakest Liberal Preconditions.
- Lecture 2 (December 19th): Expressions with effects, Types, Local
variables; Blocking semantics; Labels; Total correctness
- Lecture 3 (January 9th): Exceptions and Functions
- Lecture 4 (January 16th): Specifications Languages, Programs with Arrays
- Lecture 5 (January 23th): Machine Integers, Floating-Point Numbers
- Lecture 6 (January 30th): Numerical Algorithms
- No slides, only blackboard examples.
- Lecture 7 (February 20th): Aliasing, Call by reference, Pointer Programs
- Lecture 8 (February 27th): Pointer Programs, Separation Logic
Page generated on 2013/2/28