*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:*

- Assignment 1 (May 5 2003) [ps] [pdf]
- Assignment 2 (May 12 2003) [ps] [pdf]
- Assignment 3 (May 19 2003) [ps] [pdf] [pvs for ex 3.3]
- Assignment 4 (May 26 2003) [ps] [pdf] [pvs for ex 4.1] [pvs for ex 4.2]
- Assignment 5 (June 2 2003) [ps] [pdf] [pvs for ex 5.1] [pvs for ex 5.2] [pvs for ex 5.3]
- Assignment 6 (June 16 2003) [ps] [pdf] [multisets.pvs] [multisets.prf]
- Assignment 7 (June 23 2003) [ps] [pdf]
- Assignment 8 (June 30 2003) [ps] [pdf] [resolution.pvs] [resolution.prf]
- Assignment 9 (July 7 2003) [ps] [pdf]

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:*

- Homepage
of the
*PVS*specification and verification system - Homepage
of the
*Coq*proof assistant -
Last year's lecture
on
*interactive proof tools*(WS 2001/02)

Hans de Nivelle, 2003-04-30.