Programming methods [ LSINF2224 ]

> https://icampus.uclouvain.be/claroline/course/index.php?cid=LINF2224

• 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: model-checking, temporal logic, abstraction.

Given the learning outcomes of the "Master in Computer Science and Engineering" program, this course contributes to the development, acquisition and evaluation of the following learning outcomes:

• INFO1.1-3
• INFO2.5
• INFO5.3, INFO5.5
• INFO6.1, INFO6.3

Given the learning outcomes of the "Master [120] in Computer Science" program, this course contributes to the development, acquisition and evaluation of the following learning outcomes:

• SINF1.M3
• SINF2.5
• SINF5.3, SINF5.5
• SINF6.1, SINF6.3

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.

The contribution of this Teaching Unit to the development and command of the skills and learning outcomes of the programme(s) can be accessed at the end of this sheet, in the section entitled “Programmes/courses offering this Teaching Unit”.

• 3 assignments, 45% of the final grade.
• Theory: oral exam, 55% of the final grade. A list of questions is provided at the end of the course.

The asssignments can only be presented during the quadrimester of the course.  They cannot be represented in subsequent exam sessions.

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.

Background:

• LINGI1122