Softwareprodukte sind in den
vergangenen Jahren ein integraler Bestandteil unseres alltäglichen
Lebens geworden. Anwendungen reichen von Steuerungsmodulen in
Alltagsprodukten, e-Commerce, Telephonnetzen, 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, den
Anwendungsbereich und Programmiertechniken verwendet und zu einem
Grossteil 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 2 Semester verteilt.
Im ersten Teil (Moodle Kurs 2022) wurde die
intuitionistische Typentheorie als theoretisches Fundament vorgestellt.
Thema dieses zweiten Teils sind Aufbau, Automatisierung und Anwendung
von Beweissystemen.
