Automatisches Beweisen: Methoden und Anwendungen

Abstract

Mit der zunehmenden Verbreitung und Komplexität von Computersystemen ist Zuverlässigkeit zu einem wichtigen Thema
geworden. Dies gilt insbesondere für Computersysteme, die sicherheitskritische Funktionen implementieren, z. B. Systeme,
die in Fahrzeuge oder Flugzeuge eingebettet sind. Formale Methoden bieten eine Möglichkeit, Vertrauen in solche Systeme
zu schaffen. Insbesondere die Programmverifikation ermöglicht es uns, die Abwesenheit von Fehlern in einem System oder
seinen Komponenten nachzuweisen: mit stringenten logischen und mathematischen Methoden wird ein Beweis für die
Korrektheit eines Systems erbracht, der bestätigt, dass das System genau so funktioniert wie beabsichtigt und keine Abweichungen aufweist.