Kursbeschreibung und Literatur
Softwareprodukte
sind in den vergangenen Jahren ein integraler Bestandteil unseres
alltäglichen Lebens geworden. Anwendungen reichen von Steuerungsmodulen
in Alltagsprodukten, e-Commerce, Telefonnetzen, bis hin zu
Automobilkonstruktion und Luftfahrtkontrolle.
Die wachsende
Komplexität und umfassendere Verwendung dieser Produkte macht es
erforderlich, Methoden zu entwickeln, welche die Zuverlässigkeit von
Software besonders in sicherheitskritischen Anwendungen sicherstellen.
Aus konzeptioneller Sicht ist der Entwurf von Software im Wesentlichen
ein logischer Schlussfolgerungsprozess, der Wissen über Algorithmen,
deren Anwendungsbereich und Programmiertechniken verwendet und zu einem
Großteil schematisiert werden kann. Durch den Einsatz logisch-formaler
Methoden kann die Zuverlässigkeit dieses Prozesses erheblich gesteigert
werden.
Im Rahmen der Vorlesung Automatisierte Logik und
Programmierung werden die Grundlagen logisch-formaler
Programmentwicklung besprochen. Die Formalisierung von Logik,
Berechenbarkeit und Datentypen in der intutionistischen Typentheorie
bildet das theoretische Fundament. Die Automatisierung logischer
Schlüsse wird anhand des interaktiven Beweissystems Nuprl demonstriert.
Aufgrund des Umfangs der Thematik wird die Veranstaltung auf zwei
Semester verteilt. Schwerpunkt des ersten Semesters ist das theoretische
Fundament. Thema des zweiten Semesters sind Aufbau, Automatisierung und
Anwendung von Beweissystemen.
Literatur
- Per Martin-Löf: Intuitionistic Type Theory., Studies in Proof Theory Lecture Notes, Bibliopolis, Napoli 2002
- Robert L. Constable et. al.: Implementing Mathematics with the Nuprl proof development system. Prentice Hall, 1986
- Lawrence C. Paulson: Logic and Computation: Interactive Proof with Cambridge LCF. Cambridge University Press, 1987
- Kursleiter*in: Prof. Dr. Christoph Kreitz