Construction and Verification of Software (2021/2022)
Quick Links
Topics and Course Structure
This course is about program verification techniques, with a strong emphasis on static (i.e. compile-time) deductive verification of (mostly) imperative programs. To this end, the course emphasizes two logical systems for reasoning about imperative code: Hoare Logic and Separation Logic.
The first part of the semester covers the former, supported by the Dafny language and verification framework. We cover program specification using functional code, which includes reasoning about correctness of specification via induction, and logical assertions. Imperative code is verified using (extended) Hoare logic, covering the standard reasoning mechanisms of pre-condition, post-conditions and loop invariants. As we transition to reasoning about abstraction mechanisms such as objects, we introduce Abstract Data Types, which leads us into a range of topics such as representation invariants, type states, the framing problem and a solution in (extended) Hoare logic called Dynamic Frames.
The second part of the semester covers Separation Logic, supported by the Verifast verification tool for Java and C code. Separation Logic provides a dual answer to the framing problem of Hoare Logic, allowing for much more natural reasoning about imperative code with shared mutable state (i.e. aliasing and pointers). We also explore the problem of verification in the presence of sharing and aliasing in a concurrent setting, through the use of Monitors and higher-order predicates.
In the final lectures of the course we cover dynamic verification through Black Box and White Box testing.
The course features three projects throughout the semester, two using Dafny and one using Verifast.
Lectures
- Lecture 1 (Slides) - Introduction
- Lecture 2 (Slides, Lecture Notes) - Hoare Logic I
- Lecture 3 (Slides, Lecture Notes) - Hoare Logic II
- Lecture 4 (Slides, Lecture Notes) - Loops, Arrays and Machine Integers
- Lecture 5 (Slides, Lecture Notes) - Abstract Data Types I
- Lecture 6 (Slides, Lecture Notes) - Abstract Data Types, Framing and Typestates
- Lecture 7 (Slides) - Separation Logic I
- Lecture 8 (Slides, Lecture Notes) - Separation Logic II
- Lecture 9 (Slides) - Concurrent Abstract Data Types in Separation Logic
- Lecture 10 (Slides) - Resource Sharing and Separation
- Lecture 11 (Slides) - Dynamic Verification