Computer-Aided Modelling and Reasoning

Overview

Lecturers: Dr. Andreas Lochbihler and Dr. Christoph Sprenger

Classes: Tuesday 9-12h, in CHN D 44

Credits: 8 ECTS (7P)
All participating students will take part in a longer-term project. The final grade will be composed as follows: 50% exam and 50% project work. Computer-based exam as a session examination.

Language: English

Announcements

• We have published the grading scheme for the project including information about the end presentation on the protected page course material's web page (requires n.ethz login).
  
• Oct 27: The semester feedback starts on Oct 28 at 9:15 and ends on Nov 2. Please participate in the survey using EduApp.
• Oct 6: The computer-based exam during the Sessionsprüfung will take on Windows-based PCs. You may choose between three keyboard layouts: US, Swiss German, and Swiss French. Please tell us your preference by the last lecture on Dec 16. If you must use a different layout, you have to convince LET to provide your desired layout.
• Okt 6: Please start to look for a team partner with whom you will work on the project. If you have not found one by end of October, we will pair the unassigned students.
• Sep 17: This course will henceforth take place in a new room: CHN D 44.
• Sep 4: The class room has a number of PCs installed, but it might be more convenient to bring your own laptop. Please install external page Isabelle2014 before the first class if possible.

Description

This lab is a hands-on course about using an interactive theorem prover to construct formal models of algorithms, protocols, and programming languages and to reason about their properties. The focus is on applying logical methods to concrete problems supported by a theorem prover. The course will demonstrate the challenges of formal rigor, but also the benefits of machine support in modelling, proving and validating.
The lab will have two parts: The first introduces basic and advanced modelling techniques (functional programs, inductive definitions, modules) and the associated proof techniques (term rewriting, resolution, induction, proof automation). In the second, the students work in teams of 2-3 on a project in which they apply these techniques to a given topic: they build a formal model and prove its desired properties. The topic will be taken from the area of programming languages, model checking, or information security.

Objectives

The students learn to effectively use a theorem prover to create unambiguous models and rigorously analyse them. They learn how to write precise and concise specifications and to exploit the proof assistant as a tool for checking and analysing such models and for taming their complexity.

Requirements

none, but the following are recommended

• functional programming and logics (as taught in FMFP)
• participation (you must be willing to participate in the labs and get your hands dirty with a proof assistant)

Resources

• external page Isabelle theorem prover and external page documentation (also available from within Isabelle)
• Textbook: Tobias Nipkow, Gerwin Klein. external page Concrete Semantics, part 1
• Isabelle community support: and on external page stack overflow