Programming methods
[SINF2224]
[30h + 15h] 5 credits
This course is taught in the 2d semester.
Teacher(s): Charles Pecheur
Language: English
Level: Second
Aims
- To know and understand the techniques that allow those principles to the automated on a computer.
- To appraise through experience the potential and limits of such terchniques.
Main themes
- Deductive proof for programs: Hoare logic, weakest preconditions, verification conditions, invariants and variants.
- Automating proofs: loops, procedures and recursion, data structures, reactive program.
- State-based analysis: models-checking, temporal logic, abstraction.
The course combines lectures and assignments where students use automated verification software (ESC/Java, Java PathFinder) to prove properties of Java programs.
Content and teaching methods
Other information (prerequisite, evaluation (assessment methods), course materials recommended readings, ...)
Bibliography:
- B. Liskov (with J. Guttag), "Program development in Java: abstraction, specification and object-oriented design", Addison-Wesley, 2001
- O.-J. Dalh, "Verifiable programming", Prentice Hall, 1992
- K. R. Apt, E.-R. Olderog, "Verification of sequential and concurrent programs", Springer-Verlag, 1991
- J. Loeckx, K. Sieber, "The foundations of program verification (2nd Ed.), Wiley-Teubner, 1984
- D. Gries, The Science of Computer Programming, Springer-Verlag, 1981