Abstrakte Programme beinhalten Platzhalter, welche unendlich viele konkrete Programme repräsentieren können. Sie werden in verschiedenen, sich mit der Korrektheit von Programmen befassenden Bereichen der Informatik verwendet: Regelbasierte Kompilierung und Optimierung, Refaktorisierung von Programmen und andere Quelltexttransformationen, Programmsynthese, inkrementell-korrektheitserhaltende Konstruktion von Programmen (engl. Correctness-by-Construction), und mehr. Mechanisierte Korrektheitsargumente für abstrakte Programme werden häufig in interaktiven Beweisumgebungen durchgeführt. Dies erlaubt den Ausdruck beliebiger, über Programme quantifizierender Eigenschaften; allerdings ist es sehr aufwändig, diese manuell durch das Schreiben von Beweisskripten zu verifizieren. Bestehende automatische Beweissysteme für abstrakte Programme leiden hingegen unter einer geringen Ausdrucksstärke. Häufig unterstützen diese Systeme ausschließlich Platzhalter, welche alle möglichen Programme repräsentieren; in einigen Fällen werden geringe Verfeinerungen unterstützt.

Die vorliegende Dissertation schließt diese Lücke durch das Konzept der abstrakten Ausführung, einer automatischen Beweistechnik für universelle Verhaltenseigenschaften abstrakter Programme. Die Beschränkung auf universelle (keine existentiellen Quantoren) und Verhaltenseigenschaften (welche sich nicht auf die innere, syntaktische Struktur der Platzhalter beziehen) schließt gewisse Anwendungen aus; allerdings ermöglicht dies erst den hohen Automatisierungsgrad. Die Logik abstrakter Ausführung verwendet abstrakte Zustandsübergänge, um unbekannte Effekte auf lokale Programmvariablen und den Haufenspeicher (engl. heap) zu modellieren; für abrupte Terminierung werden symbolische Fallunterscheidungen durchgeführt. Platzhalter haben Namen: Dies erlaubt ihre Verwendung an verschiedenen Stellen, wo sie die selben Programmelemente in möglicherweise unterschiedlichen Kontexten repräsentieren. Zusätzlich können Instantiierungen durch eine ausdrucksstarke Spezifikationssprache begrenzt werden. Diese ist ein auszeichnendes Merkmal abstrakter Ausführung. Der Einsatz der Theorie dynamischer Rahmen (engl. dynamic frames) ermöglicht es, beschreibbare Speicherbereiche beliebig präzise anzugeben. Das System unterstützt Nachbedingungen sowie feingranulare Vorbedingungen für abrupte Terminierung.

Abstrakte Ausführung ist im Programmbeweiser KeY implementiert. Speziell für die Verifikation relationaler Programmeigenschaften wurde REFINITY entwickelt, eine grafische Benutzeroberfläche als Erweiterung von KeY. Diese wurde in der bisher wichtigsten Anwendung abstrakter Ausführung eingesetzt: der Modellierung bekannter Refaktorisierungstechniken auf Anweisungsebene (engl. statement-level), deren Korrektheit unter Bedingungen bewiesen wurde. Diese Fallstudie brachte mehrere, bisher undokumentierte Vorbedingungen für die sichere (engl. safe) Anwendung von Refaktorisierung hervor, und ist damit einer der wenigen Versuche, statisch die (semantische) Korrektheit von Refaktorisierungstechniken auf Anweisungsebene zu beweisen, und der einzige, welcher es in diesem Umfang vermochte.

Als Beitrag zum formalen Fundament abstrakter Ausführung enthält diese Arbeit eine allgemeine Theorie symbolischer Ausführung basierend auf der Semantik symbolischer Zustände. Zustandsverschmelzung (engl. state merging) wird direkt unterstützt, da das formale System auf m-zu-n-Zustandsübergängen beruht. Ein wichtiger Beitrag sind zwei orthogonale Korrektheitsbegriffe, Abdeckung (engl. exhaustiveness) und Präzision, deren Zusammenhang zu deduktiven Programmbeweisen und automatisierter Fehlersuche formal bewiesen wird.

Schließlich beschreibt diese Ausarbeitung die modale Zustandssequenzlogik (engl. Modal Trace Logic) (MTL), eine auf Zustandssequenzen (engl. traces; Aufzeichnungen während einer Programmausführung anfallender Zustände. Wird auch mit Spuren übersetzt.) beruhende Logik zur Repräsentation unterschiedlicher Programmverifikationsprobleme, insbesondere für relationale Verifikation. Es handelt sich um ein flexibles System, welches nach Bedarf um formale Sprachen mit Zustandssequenzsemantik erweitert werden kann. Der Hauptbestandteil von MTL ist die Zustandssequenzmodalität, (engl. trace modality) welche ausdrückt, dass eine Spezifikation eine Implementierung nach einem Abstraktionsschritt approximiert. Die Vielseitigkeit dieses Formalismus wird durch die Anwendung auf eine Reihe von Problemfeldern demonstriert, darunter u.A. funktionale Verifikation, Programmsynthese und Programmevolution. Um MTL-Probleme mechanisiert zu beweisen, übersetzen wir sie in symbolische Zustandssequenzen. Speziell für diese wurde die symbolische Zustandssequenzlogik (engl. Symbolic Trace Logic) (STL) eingeführt, welche über einen Sequenzenkalkül zum Beweisen von Teilmengeneigenschaften symbolischer Zustandssequenzen verfügt. Dieser erfordert die Analyse von symbolischen Zuständen auf "Subsumption". Die Basis dafür besteht in zwei allgemeinen, neuen Subsumptionsbegriffen. MTL und STL verhalten sich wie folgt zu den restlichen Bestandteilen dieser Dissertation: Um Programmsynthese und Kompilierung zu formalisieren, wird die Sprache abstrakter Programme verwendet, was MTL mit abstrakter Ausführung verbindet. Weiterhin basieren symbolische Zustände in STL auf der Theorie symbolischer Ausführung.