MOVES Seminar, 28 Juni 2006, 14:00

Automatisierung von Induktionsbeweisen zur Verifikation funktionaler Programme (Diplomarbeitsvortrag, in German)


Ralf Behle

Zusammenfassung:

 

Allgemein ist die Verifikation von Programmen bedeutsam, um den Betrieb von Software in kritischen Bereichen garantieren zu können. Ein Schwerpunkt der Verifikation ist dabei die Verifikation der partiellen Korrektheit. Hierfür wurden in der Vergangenheit verschiedenen automatische Techniken entwickelt.

In diesem Vortrag liegt der Fokus auf der Analyse der partiellen Korrektheit einfacher funktionaler Programme, unter der Verwendung von automatisierten Induktionsbeweisen.