Construction and Verification of Software (2021/2022)

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.