Close Help Print
 Course module: 202100126
 202100126Interactive Theorem Proving
 Course info
Course module202100126
Credits (ECTS)5
Course typeCourse
Language of instructionEnglish
Contact persondr. P. Lammich
E-mailp.lammich@utwente.nl
Lecturer(s)
 Lecturer B. Kohlen Examiner dr. P. Lammich Contactperson for the course dr. P. Lammich Lecturer dr. P. Lammich
Starting block
 1B
Application procedureYou apply via OSIRIS Student
Registration using OSIRISYes
 Aims
 body { font-size: 9pt; font-family: Arial } table { font-size: 9pt; font-family: Arial } Upon completion of the course, the student will be able to: develop formal proofs in Isabelle/HOL develop formal specifications for given problems explain the idea of abstract data types and refinement analyze algorithms using ADTs and stepwise refinement verify simple algorithms with Isabelle/HOL, using stepwise refinement
 Content
 body { font-size: 9pt; font-family: Arial } table { font-size: 9pt; font-family: Arial } 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 a 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 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 (2017000117)   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.
 Participating study
 Master Computer Science
Required materials
Book
 Concrete Semantics: With Isabelle/HOL , Tobias Nipkow, Gerwin Klein (online version) - http://concrete-semantics.org/
Recommended materials
Book
 Concrete Semantics: With Isabelle/HOL , Tobias Nipkow, Gerwin Klein (hard copy) - ISBN 978-3319105413
Instructional modes
Assignment
 Presence duty Yes

Lecture
 Presence duty Yes

Tutorial
 Presence duty Yes

Tests