Program Verification

• specify functional correctness properties of imperative programs;
• use automated verification tools to develop formally verified software;
• justify why a program meets its specification based on sound reasoning principles;
• explain the technology stack involved in building automated verification tools;
• compare deductive program verification to other methods aiming at increasing confidence in software correctness;
• encode verification-related decision problems to SMT (satisfiability modulo theories);
• identify potential bottlenecks in existing SMT encodings;
• construct sound methodologies for program verification problems, automate these methodologies via encodings to SMT, and justify the involved design decisions;
• achieve the above goals in a group effort while at the same time maintaining individual accountability; and
• communicate solutions to problems in a clear and precise manner.

The course covers reasoning principles, technologies, and design decisions underlying automated deductive verification tools. In particular, it introduces
(1) program logics for writing formal correctness proofs (for example weakest preconditions and separation logic);
(2) SMT solvers (for example Z3) for automating reasoning about logical formulas;
(3) intermediate verification languages (for example Viper) for encoding verification methodologies; and
(4) source code verifiers for handling feature-rich programming languages.
The course will intermix technical content with hands-on experience.

02141, Basic familiarity with program semantics and predicate logic is expected; the necessary background can be obtained in the course 02141. Students must be fluent in at least one object-oriented or functional programming language. Courses involving mathematical logic, for example 02156, are an advantage.

Lectures, exercises, and project work.