Sluiten Help Print
 Cursus: 202100126
 202100126Interactive Theorem Proving
 Cursus informatie
Cursus202100126
Studiepunten (ECTS)5
CursustypeCursus
VoertaalEngels
Contactpersoondr. P. Lammich
E-mailp.lammich@utwente.nl
Docenten
 Docent B. Kohlen Docent dr. P. Lammich Examinator dr. P. Lammich Contactpersoon van de cursus dr. P. Lammich
Collegejaar2021
Aanvangsblok
 1B
AanmeldingsprocedureZelf aanmelden via OSIRIS Student
Inschrijven via OSIRISJa
 Cursusdoelen
 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
 Inhoud
 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
Verplicht materiaal
Book
 Concrete Semantics: With Isabelle/HOL , Tobias Nipkow, Gerwin Klein (online version) - http://concrete-semantics.org/
Aanbevolen materiaal
Book
 Concrete Semantics: With Isabelle/HOL , Tobias Nipkow, Gerwin Klein (hard copy) - ISBN 978-3319105413
Werkvormen
Hoorcollege
 Aanwezigheidsplicht Ja

Opdracht
 Aanwezigheidsplicht Ja

Werkcollege
 Aanwezigheidsplicht Ja

Toetsen