Formal framework for proof generating optimizers [Elektronische Ressource] / von Marek Jerzy Gawkowski

Formal Framework forProof Generating OptimizersVom Fachbereich Informatikder Universität Kaiserslauternzur Verleihung des akademischen GradesDoktor der Naturwissenschaften (Dr. rer. nat.)genehmigte DissertationvonMarek Jerzy GawkowskiNovember 25, 2008Termin der wissenschaftlichen Aussprache: 20.04.2009Dekan: Prof. Dr. Karsten BernsVorsitzender des Prüfungsausschusses: Prof. Dr. Karsten Berns1. Berichterstatter: Prof. Dr. Arnd Poetzsch-He!ter2. Berich Prof. Dr. Klaus SchneiderD 386VZusammenfassung. Ein Softwaresystem wird meistens entweder in einer Spezifikations- oder einerhöheren Programmiersprache geschrieben. Dessen Laufzeitverhalten wird jedoch durch den Maschinen-code, der das Ergebnis der Übersetzung seiner Beschreibung in einer höheren Quellsprache ist, bestimmt.Für ein unkritisches Softwaresystem mag es ausreichen, dieses auf die Abwesenheit der Fehler durch Über-prüfungvonTestläufenzutesten.FüreinsicherheitskritischesSoftwaresystemkommenjedocherschwerendzwei Faktoren hinzu. Erstens, der Software-Producer, der dieses Softw implementiert hat, mussformal nachweisen, dass sein Maschinencode die formale Spezifikation, die vom Software-Consumer aus-gestelltwirdundseineSafety-Policy beschreibt,erfüllt.Zweitens,dieQuellsprachenbeschreibungdesSoft-waresystemsistdasErgebnisderAnwendungderstatischenAnalyseundformalerMethoden,welchedieseBeschreibung in Richtung E!zienz und Korrektheit optimieren.