Software is notoriously error-prone, and even with systematic testing, it's practically impossible to find all bugs. An alternative to testing is to mathematically prove that a program is correct. However, mathematical proofs, in particular those for program correctness, tend to get large, unreadable, and error-prone themselves, when executed with pen and paper. This can be mitigated by interactive theorem provers (ITPs), which are software systems that check mathematical proofs for correctness, and help the user develop such proofs. Many ITPs are designed such that proofs must be accepted by a small and well-tested logical inference kernel. Thus, theorems proved by ITPs are very likely to be correct.
This course introduces the state-of-the-art interactive theorem prover Isabelle/HOL and its application to the verification of simple computer programs.
The main objective is to teach the students to use ITPs on their own, thus the main focus will be on hands-on exercises and practical homework.
The course is roughly structured in three parts:
- Introduction to Functional Programming and Isabelle/HOL
This part introduces functional programming and the basic usage of the Isabelle/HOL theorem prover.
We will prove correct some simple functional data structures, and some basic theorems from graph theory.
- Abstract Data Types and Implementations
In this part, we will show how to naturally reason about algorithms by separating the abstract algorithmic idea from the actual data structures used for implementation. This separation of concerns makes correctness proofs of algorithms more manageable and allows a higher level of re-usability.
We will prove correct some simple graph algorithms (e.g. DFS).
- Nondeterministic Programs and Refinement
In the last part, we introduce stepwise refinement, which generalizes the idea from Part II to allow multiple steps from the algorithmic idea to the implementation.
We will formalize a nondeterminism/error monad to express programs, and a syntax-directed verification condition generator to automate some parts of the correctness proofs.
As an application example, we will prove correct a slightly more complex algorithm from graph theory, (e.g., Dijkstra's shortest paths).
Entry requirements
- Basic knowledge of first-order logic, basics of program specifications (pre- and postconditions).
This is covered in, e.g., the UT bachelor course Software Systems (202001024)
- Datastructures and Algorithms: (e.g. trees, search trees, tree traversal (DFS, BFS)).
This is covered in, e.g., the UT bachelor course Algorithms, Datastructures and Complexity (202001182)
- Optional: functional programming
This is covered in, e.g., the UT bachelor course Programming Paradigms (202001039).
A brief introduction to the required aspects of FP will be given at the beginning of this course.
|