Software Construction and Verification
Objectives
Knowledge
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
Code
11159
Credits
6.0
Responsible teacher
Carla Maria Gonçalves Ferreira, Mário José Parreira Pereira
Hours
Weekly - 4
Total - 52
Teaching language
Português
Prerequisites
Available soon
Bibliography
Software Foundations: https://softwarefoundations.cis.upenn.edu/
Coq reference manual: https://coq.inria.fr/distrib/current/refman/
Many books, tutorials and videos about Coq: https://coq.inria.fr/documentation
Why3 reference manual: https://why3.lri.fr/manual.pdf
Many tutorials on Why3: https://why3.lri.fr/
Software Foundations, Volume 6: https://softwarefoundations.cis.upenn.edu/slf-current/index.html
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: https://wikimpri.dptinfo.ens-cachan.fr/doku.php?id=cours:c-2-36-1
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.