Program semantics and verification

Course goals

Learning goals: to become familiar with, and acquire insight on the underlying concepts of:

• program semantics: axiomatic.
• formalisms to express programs' correctness: Hoare-style, LTL, and CTL.
• automated verification techniques: predicate transformation/symbolic execution, automated theorem proving, and model checking (LTL,CTL, symbolic).

Additionally, to acquire hands-on experience with : 

• implementing and optimizing a verification technique.
• using selected verification tools to model a problem and conduct a verification of its solution.

Assessment
In principle assignments (20% of the final mark), projects (25%), exams (55%).

This can be changed depending on the composition of the project, but in any case the exam form and grading will be announced and fixed at the start of the course.

To qualify for a repair of the final result the mark needs to be at least a 4, or “AANV”.

Content

Most modern software is quite complex. The most widely used approach to verify them is still by testing, which is inherently incomplete and hard to scale up to cover the complexity. In this course we will discuss a number of advanced validation and verification techniques that go far beyond ad-hoc testing.
Exploiting them is an important key towards more reliable complex software.

We will in particular focus on techniques that can be automated, or at least partially automated: 

• predicate transformation technique, which you can use to symbolically execute a program to calculate its range of input or output. This leads to  bounded but symbolic and fully automated verification techniques.
• common automated theorem proving techniques, used as the back-end of symbolic execution based verification.
• model checking techniques, that can be used to either fully verify a model of a program, even if the number of possible executions is infinite, or to boundedly verify the program itself.

Course form
Lectures, projects.