Programming methods [ LSINF2224 ]

> https://www.icampus.ucl.ac.be/claroline/course/index.php?cid=LINF2224

• basic notions in theory of programming, as covered in courses such as INGI1122 (Program conception methods), INGI1101 (Logic and discrete structures) and INGI1123 (Calculability)

• Program foundations and properties, semantics, validity and proof.
• 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.

Students completing successfully this course will be able to

• define and formalize the principles of program analysis and verification introduced in bachelor courses.
• describe and apply the techniques that allow those principles to be automated on a computer.
• illustrate the potential and limits of such techniques using pratical examples.

Students will have developed skills and operational methodology. In particular, they have developed their ability to

• formalize in mathematical form a given problem;
  
• write a brief technical report covering the main elements of an analysis;
• argue orally.

• Assignments (50% of final grade)
  
• oral examination based on a list of questions (available at the end of the semester) (50% of final grade)

The course combines

• lectures,
• exercises (modeling and analysis of programs),
• and assignments where students use automated verification software (ESC/Java, Java PathFinder) to prove properties of Java programs.

The aims, methodology and tools used in each assignment are described in a document provided to the students. The program code to be analyzed is commented and a brief user's guide is included. The program verification and model-checking tools to be used are clearly indicated. To ease their grip by students, exercise sessions are planned. In addition, a consultancy is provided by the supervisors of the course in case of trouble. At the end of each mission, students write a brief report used as a basis for evaluation.

1. Demonstration
2. Introduction
3. Foundations
4. Sequential Programs
5. Verification Conditions
6. Procedures
7. Recursion
8. Data Structures
9. Reactive Programs
10. State-Based Models
11. Model Checking
12. Abstraction

Support material :

• copies from lecture slides

Bibliography :

• B. Liskov, J. Guttag. Program Development in Java: Abstraction, Specification and Object-Oriented Design. Addison-Wesley, 2001.
• O.-J. Dahl. 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.