Time and Venue:
Lecture: Mondays, 11:15--13:00 Uhr, Bldg 45, Room 003
Tutorial: Mondays, 16:15--18:00 Uhr, Bldg 46 (MPI), Room 023
Lecturers:
Hans de Nivelle
Patrick Maier
Description:
We discuss methods and tools for formally proving correctness
of mathematical proofs and hardware or software systems.
Guaranteed correctness is necessary for safety-critical applications
(e.g. anti-blocking systems in cars, autopilots in airplanes)
as well as for any other system where failure causes large economical
damage (e.g. banking systems, aqua-stops in washing machines).
Verifying a complex system must include verification of the mathematical background theory, therefore it requires the development of formal mathematical models. In order to express the relevant properties that one wishes to prove, one needs higher-order logic. Without higher-order, many properties (e.g. inductive invariants) cannot be expressed and reasoned about in a natural way. In software engineering, identifying the appropriate classes for the underlying problem is an art that requires experience, insight and good taste. In verification, finding the right invariants is a similar art.
In the lecture, we explain the principles of higher-order logic, its relation to typed lambda calculus, and how an interactive theorem prover for higher-order logic can be implemented. Besides, we develop modeling and verification skills by verifying many examples with state-of-the-art theorem provers.
Practical exercises will be done with two tools, Coq and PVS. These systems have different philosophies: Coq formalizes higher-order logic with inductive types, which gives a rigorous notion of proof (Curry-Howard isomorphism). On the other hand, PVS lacks such a rigorous notion of proof but it incorporates powerful automatic decision procedures.
Download slides and supplementary material (PVS files, ...)
Assignments:
Download solutions to the assignments
Exam:
Monday, July 21, 11:15--13:00 Uhr, Bldg 45, Room 003
It is allowed to use course notes during the exam,
but we do not allow the use of computers or other electronic devices.
Results of the exam have been sent to the participants
via email.
References: