Zum Inhalt
Fakultät für Informatik

Aktuelle Themen im logikbasierten Software Engineering

Beginn: Ende: Veranstaltungsort: Vorlesung: OH12-R3.031 / Übung: Online
  • Lehrveranstaltungen
Veranstalter: Dr. Andrej Dudenhefner
Typ: Vertiefungsmodul Master
Modulnummer: INF-MSc-327
SWS: Vorlesung: 2 SWS 
Übung: 2 SWS
Ort: Vorlesung: OH12/R3.031
Übung: Online
Zeit: Vorlesung: Mo 10-12
Übung: Mi 12-14
Beginn: Vorlesung: 03.04.2023
Übung: 12.04.2023
Übung: siehe Moodle
Studienleistung: 50% erreichbarer Punkte in Übungen
Prüfungsleistung: Mündliche Prüfung


Since about the beginning of the 21st century, formal proof has become one of the standard methods in industrial hardware verification, particularly in CPU verification (Intel, AMD). During the past decade, the proof assistant technology has matured enough to also enable formal certification of substantial software systems. Two major success stories are the seL4 operating system microkernel and the CompCert optimising Clight compiler. Recently, deductive program verification has begun to attract increasing attention in the software industry (Microsoft, Amazon, Facebook, Galois). To quote Nikhil Swamy from Microsoft Research:

"Today, what seemed impossible just a few years ago is becoming a reality. We can, in certain domains, produce fully verified software at a nontrivial scale and with runtime performance that meets or exceeds the best unverified software."

This lecture is about writing functional programs in Coq and proving them correct.

Coq - the 2013 ACM Software System Award winner - is an interactive proof assistant for the development of mathematical theories and formally certified software. Its underlying theory is the Calculus of Inductive Constructions - a variant of dependent type theory with inductive types. The lecture covers programming and proving in Coq, dependent type theory, and applications to program verification. The overlap with LMSE 1 & 2 is minimal and no familiarity with type theory is necessary. In LMSE the emphasis is on "simpler" type theories, and only the basics of Coq and dependent type theory are treated there. ATLSE focuses on dependently typed functional programming, verification of functional programs, proof automation, theoretical foundations of inductive and dependent types.


Some experience with functional programming and formal logic. You should understand mathematical induction. If you liked the logic and/or the functional programming bachelor courses then this lecture is for you. If you're interested in formal methods and security then this may also be for you. The lecture is self-contained - knowledge of type theory or previous participation in LMSE are not necessary.

Supplementary Materials