Software Construction and Verification



The students consolidate their software construction skills for building trustworthy software, in the broad context of modern software systems.

The CU develops the perspective that verification should be tightly integrated with the software construction process, guided by the use of code analysis tools.

Core techniques for the static analysis of code are covered, namely verification of functional programs, the use of Hoare Logic, and the use of Separation Logic.

Knowledge Application

Use rigorous programming methods and verification techniques to ensure the reliability of software.

Develop, in team work, mid-size projects that require developing the specification and verified implementation of non-trivial algorithms and programs.

Use logical assertions to specify, verifiy, and reason about programs correctness, as well as associated tools (Coq, Why3, CFML).

Specify behavioral specifications (invariants, pre-conditions, and post-conditions) to implement modules and their interfaces. 

General characterization





Responsible teacher

Carla Maria Gonçalves Ferreira, Mário José Parreira Pereira


Weekly - 4

Total - 52

Teaching language



Available soon


Software Foundations:

Coq reference manual:

Many books, tutorials and videos about Coq:

Why3 reference manual:

Many tutorials on Why3:

Software Foundations, Volume 6:

Several classical papers by Liskov, Hoare, Dijkstra, Brinch Hansen, Doug Lea, O’Hearn, Schneider.

Related course at the Parisian Master of Research in Computer Science:

Teaching method

Students learn about the main concepts during lectures. Lab sessions are mainly devoted to the resolution of problems and exercises.

Lectures present the core concepts of the course: verification of functional programs, Hoare Logic, weakest precondition calculus, and Separation Logic.

During lab sessions students use software deductive verification tools to solve exercises and implement small-mid size verified programs.

Evaluation method

Grading Components

The grading is made up of two components: laboratory and theoretical-practical.

Laboratory Component

The laboratory component comprises three handouts and weights 60% of the final
grade. Each handout consists of in the design of a formally verified program
(i.e., specification plus implementation). Such handouts are done in teams of
two students, and the grading might be subject to eventual discussion.

The laboratory component grade (LComp) is the mean of the three handouts grades
(HO1, HO2, and HO3):

LComp = (HO1 + HO2 + HO3) / 3.

In order to succeed, it is required that LComp >= 9.5.

Theoretical-Practical Component

The theoretical-practical component comprises two tests (lectures period) or a
final exam. Tests and exams are written, open-book and done in person and
individually. This component weights 60% of the final grade.

The theoretical-practical grade (TPComp) is the mean of the tests (T1 and T2) of
the exam grade (Ex):

TPComp = (T1 + T2) / 2 or TPComp = Ex.

In order to succeed, it is required TPComp >= 9.5.

Final Grade

The final grade (F), defined only if LComp >= 9.5, is:

  • F = TPComp, if TPComp < 9.5;
  • F = 0.4 LComp + 0.6 LComp, if TPComp >= 9.5.

All grade (HO1, HO2, HO3, T1, T2, Ex, LComp, TPComp) are rounded towards the
nearest tenth, except the final grade (F) which rounded towards the nearest
whole number.

Subject matter

1. Verification of functional programs

Algebraic reasoning about stateless programs. Proofs by induction. Definition and use of inductive propositions. Induction principles. Verification of non-trivial data structures using algebraic reasoning.

2. Verification of imperative programs

Assertions and Hoare Logic based methods. Weakest precondition calculus. Programming with arrays. Ghost code. Treatment of exceptions. Modularity. Specification of data structures using a logical representation models. Treatment and static control of aliasing.

3. Verification of heap-dependent programs

Separation Logic. Heap predicates. Frame rule. Representation predicates for lists and trees. List segments. Reasoning about functions. Higher-order functions and iteration. Higher-order representation predicates. Introduction to Concurrent Separation Logic.


Programs where the course is taught: