Computer-Aided Modelling and Reasoning

Overview

Lecturer: Dr. Christoph Sprenger
Assistant: Shabnam Ghasemirad

Classes: Thursdays 10-14, HG E 33.5

Credits: 8 ECTS
All participating students will take part in a mandatory longer-term project. The project will span the second half of the semester. As a preparation for the project, students must hand in their solutions to 5 of 7 exercise sheets accompanying the lectures. Apart from this, the performance assessment will be based on the project work.

Language: English

Announcements

• Last deregistration date is March 31. After this date a deregistration will be counted as failure. This information has also been added to the course catalog.
• Please install external external pageIsabelle2022call_made on your laptop before the first class and bring your laptop to 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 two 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

No formal requirements, 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 pageIsabelle theorem provercall_made and external pagedocumentationcall_made (also available from within Isabelle)
• Textbook: Tobias Nipkow, Gerwin Klein. external pageConcrete Semanticscall_made, part 1
• Isabelle community support: and on external pagestack overflowcall_made