The "computer-aided modelling and reasoning" 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 lab has two parts: The first introduces various modelling and proof techniques. The second part consists of a project in which the students apply these techniques
Lernziel
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.
Inhalt
The "computer-aided modelling and reasoning" 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.
Leistungskontrolle
Information zur Leistungskontrolle (gültig bis die Lerneinheit neu gelesen wird)
Die Leistungskontrolle wird nur in der Session nach der Lerneinheit angeboten. Die Repetition ist nur nach erneuter Belegung möglich.
Prüfungsmodus
schriftlich 90 Minuten
Zusatzinformation zum Prüfungsmodus
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.
Hilfsmittel schriftlich
Keine
Diese Angaben können noch zu Semesterbeginn aktualisiert werden; verbindlich sind die Angaben auf dem Prüfungsplan.