HOME | DEUTSCH | IMPRESSUM | KIT

Theorem provers and their applications

Description only available in german.

Material

Schedule

begin 21.04.2009, end 23.07.2009

Weekday Begin End Location
Thursday 8:45h 9:30h R -143, 50.34

Schedule

Date Topic Slides Papers
21.4. (11.30h)Einleitung[PDF]
23.4. (8.45h)Die Theorembeweiser dieser Welt[PDF]F. Wiedijk: The Seventeen Provers of the World
30.4. (8.45h)Anwendungen in der Mathematik (1)[PDF]G. Gonthier: A computer-checked proof of the Four Colour Theorem
7.5. (8.45h)Anwendungen in der Mathematik (2)[PDF]J. Avigad et al.: A formally verified proof of the prime number theorem
W. McCune: Solution of the Robbins Problem
14.5. (8.45h)Anwendungen in der Mathematik (3)[PDF]T. C. Hales: Cannonballs and honeycombs
T. Nipkow et al.: Flyspeck I: Tame Graphs
28.5. (8.45h)Protokollverifikation (1)[PDF]L. C. Paulson: The Inductive Approach to Verifying Cryptographic Protocols
4.6. (8.45h)Protokollverifikation (2)[PDF]G. Bella, L. C. Paulson: Kerberos version IV: inductive analysis of the secrecy goals
25.6. (8.45h)Semantik und Typsysteme (1)[PDF]G. Klein, T. Nipkow: A machine-checked model for a Java-like language, virtual machine, and compiler
2.7. (8.45h)Semantik und Typsysteme (2)[PDF]D. Wasserrab et al.: An Operational Semantics and Type Safety Proof for Multiple Inheritance in C++
9.7. (8.45h)Typbasierte Informationsflusskontrolle[PDF]D. Volpano et al.: A sound type system for secure flow analysis
16.7. (8.45h)Compilerverifikation (1)[PDF]X. Leroy, S. Blazy: Formal Verification of a C-like Memory Model and Its Uses for Verifying Program Transformations
S. Blazy et al: Formal Verification of a C Compiler Front-End
23.7. (8.45h)Compilerverifikation (2)[PDF]X. Leroy: Formal certication of a compiler back-end or: programming a compiler with a proof assistant
X. Leroy: A formally veried compiler back-end

Personnel

Department Head
Prof. Gregor Snelting
Former Staff Member
Dr.-Ing. Daniel Wasserrab