CloseHelpPrint
Kies de Nederlandse taal
Course module: 202100126
202100126
Interactive 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
Contactperson for the course
dr. P. Lammich
Examiner
dr. P. Lammich
Academic year2022
Starting block
1B
Application procedureYou apply via OSIRIS Student
Registration using OSIRISYes
Aims
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
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:
  1. 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.
  1. 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).
  1. 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.
 
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 dutyYes

Lecture
Presence dutyYes

Tutorial
Presence dutyYes

Tests
Final exam, graded homework

CloseHelpPrint
Kies de Nederlandse taal