Coronakrise

Wegen der Coronakrise wird die Veranstaltung voraussichtlich (zumindest am Anfang des Semesters) virtuell stattfinden, d.h. über Videokonferenz. Deshalb ist es wichtig, dass ich vorher die Kontaktdaten der Teilnehmer habe. Wenn Sie an dieser Veranstaltung teilnehmen möchten, bitte melden Sie sich schnellstmöglich auf Moodle an. Wenn Sie noch nicht sicher sind, aber zumindest die erste Vorlesung hören möchten, melden Sie sich auch an.

Weitere Informationen und Neuigkeiten werden auf Moodle und per Email angekündigt.

Sprache

In the absence of strong opposition from the students, the lecture will be held in English. It is possible to talk with the lecturer in German if there is such a need, but most materials are in English anyway.

Description

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 deductive program verification with Coq. By verification we mean a full proof that a program satisfies a given specification.

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 assumed. 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 and imperative programs, formal program semantics, proof automation, theoretical foundations of inductive and dependent types.

Plan of the lecture

1. Overview. Functional programming in Coq. Polymorphism. Higher-order functions. Dependently typed functions.
2. Review of formal logic. Classical vs intuitionistic logic. Curry-Howard isomorphism. The tactic language.
3. Higher-order logic. Choice and extensionality axioms. Diaconescu's theorem. Basic proofs by induction.
4. Dependent types. Calculus of Constructions. Universes. Predicativity vs impredicativity. Proof irrelevance. Axioms and computation. Inductive specifications.
5. Dependent inductive types. Inductive predicates. Foundations of inductive types. Coinductive types.
6. Definitional vs propositional equality. Setoids. Streicher's axiom K and Uniqueness of Identity Proofs. John Major equality. Executable specifications.
7. Automation. Programming in Ltac. CoqHammer and SMTCoq.
8. Certified functional programming. The "Program" and the "Equations" packages. Program extraction.
9. Proof by reflection.
10. Certified functional AVL trees.
11. Verifying imperative programs. Formal semantics.
12. Hoare logic and Frama-C.

Prerequisites

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, particularly for embedded systems, then this may also be for you. The lecture is self-contained - knowledge of type theory or previous participation in LMSE are not necessary.

Klausur und Studienleistung

Am 01. Juli wird eine Formalisierungsaufgabe herausgegeben. Die Aufgabe soll bis 10. August abgegeben werden. Alle Studierende die zeitlich eine vernünftige Lösung abgeben, bekommen die Studienleistung. Das Projekt muss dann bis 30. September auf einer mündlichen Prüfung (Klausur) präsentiert werden. Die Note basiert auf der Qualität der Präsentation und der präsentierten Lösung.

Materials

• Certified Programming with Dependent Types and Formal Reasoning About Programs by Adam Chlipala
• Software Foundations by Benjamin C. Pierce et. al.
• Interactive Theorem Proving and Program Development (Coq'Art: The Calculus of Inductive Constructions) by Yves Bertot and Pierre Casteran
• Proof Assistants using Dependent Types by Herman Geuvers and Henk Barendregt
• Inductive definitions in the system Coq: rules and properties by Christine Paulin-Mohring
• Lectures on the Curry-Howard Isomorphism by Morten Heine B. Sorensen and Pawel Urzyczyn
• History of Interactive Theorem Proving by John Harrison, Josef Urban and Freek Wiedijk