Program testing can be used to show the presence of bugs, but never to show their absence! - Edsger W. Dijkstra, 1970
Beware of bugs in the above code; I have only proved it correct, not tried it. - Donald E. Knuth, 1977
As the world increasingly depends on software, e.g., to control our finances, drive our cars, and manage our medical devices, how can we tell whether that software will be correct, secure, or reliable? Testing for such properties is theoretically impossible, and notoriously difficult and ineffective in practice. Software verification can, in principle, provide such guarantees with the certainty of a mathematical proof. While verification has historically been difficult to apply at the scale of realistic software systems, a series of recent advances suggests we may be at an inflection point, as various research groups have successfully proven rigorous properties about critical software components, including OS kernels, compilers, and distributed systems.
The course will provide a broad introduction into the field of formal methods and verification. We will introduce the key ideas of this active research field: its motivation, the chief problems it aims to solve, and the main algorithmic techniques and ideas that have been developed to tackle these problems. We will also become familiar with some practical formal verification tools, including SAT solvers, SMT solvers, and program verifiers.
A tentative list of topics to be covered: SAT Solving - DPLL and CDCL; SMT Solving - DPLL(T) and Nelson-Oppen; Hoare Logic; Weakest Precondition Calculus; Abstract Interpretation; Model Checking, Interpolation, and IC3/PDR; Recent advances in verification of distributed systems and in application of large language models in verification.
The final grade will be composed of 50% homework assignments, and 50% final project. The homework assignments are individual, and the final project can be completed in teams of two students. The course includes 2 hours of lecture per week but counts as 3 credit points as the homework and final project will require significant dedication.
The course draws inspiration from the following courses: