TU Darmstadt / ULB / TUbiblio

Abstract Execution: Automatically Proving Infinitely Many Programs

Steinhöfel, Dominic (2020)
Abstract Execution: Automatically Proving Infinitely Many Programs.
Technische Universität Darmstadt
doi: 10.25534/tuprints-00008540
Dissertation, Erstveröffentlichung

Kurzbeschreibung (Abstract)

Abstract programs contain schematic placeholders representing potentially infinitely many concrete programs. They naturally occur in multiple areas of computer science concerned with correctness: rule-based compilation and optimization, code refactoring and other source-to-source transformations, program synthesis, Correctness-by-Construction, and more. Mechanized correctness arguments about abstract programs are frequently conducted in interactive environments. While this permits expressing arbitrary properties quantifying over programs, substantial effort has to be invested to prove them manually by writing proof scripts. Existing approaches to proving abstract program properties automatically, on the other hand, lack expressiveness. Frequently, they only support placeholders representing all possible instantiations; in some cases, minor refinements are supported.

This thesis bridges that gap by presenting Abstract Execution (AE), an automatic reasoning technique for universal behavioral properties of abstract programs. The restriction to universal (no existential quantification) and behavioral (not addressing internal structure) properties excludes certain applications; however, it is the key to automation. Our logic for Abstract Execution uses abstract state changes to represent unknown effects on local variables and the heap, and models abrupt completion by symbolic branching. In this logic, schematic placeholders have names: It is possible to re-use them at several places, representing the same program elements in potentially different contexts. Furthermore, the represented concrete programs can be constrained by an expressive specification language, which is a unique feature of AE. We use the theory of dynamic frames to scale between full abstraction and total precision of frame specifications, and support fine-grained pre- and postconditions for (abrupt) completion.

We implemented AE by extending the program verifier KeY. Specifically for relational verification of abstract Java programs, we developed REFINITY, a graphical KeY frontend. We used REFINITY it in our signature application of AE: to model well-known statement-level refactoring techniques and prove their conditional safety. Several yet undocumented behavioral preconditions for safe refactorings originated in this case study, which is one of very few attempts to statically prove behavioral correctness of statement-level refactorings, and the only one to cover them to that extent.

AE extends Symbolic Execution (SE) for abstract programs. As a foundational contribution, we propose a general framework for SE based on the semantics of symbolic states. It natively integrates state merging by supporting m-to-n transitions. We define two orthogonal correctness notions, exhaustiveness and precision, and formally prove their relation to program proving and bug detection.

Finally, we introduce Modal Trace Logic (MTL), a trace-based logic to represent a variety of different program verification tasks, especially for relational verification. It is a “plug-in” logic which can be integrated on-demand with formal languages that have a trace semantics. The core of MTL is the trace modality, which allows expressing that a specification approximates an implementation after a trace abstraction step. We demonstrate the versatility of this approach by formalizing concrete verification tasks in MTL, ranging from functional verification over program synthesis to program evolution. To reason about MTL problems, we translate them to symbolic traces. We suggest Symbolic Trace Logic (STL), which comes with a sequent calculus to prove symbolic trace inclusions. This requires checking symbolic states for subsumption; to that end, we provide two generally useful notions of symbolic state subsumption. This framework relates as follows to the other parts of this thesis: We use the language of abstract programs to express synthesis and compilation, which connects MTL to AE. Moreover, symbolic states of STL are based on our framework for SE.

Typ des Eintrags: Dissertation
Erschienen: 2020
Autor(en): Steinhöfel, Dominic
Art des Eintrags: Erstveröffentlichung
Titel: Abstract Execution: Automatically Proving Infinitely Many Programs
Sprache: Englisch
Referenten: Hähnle, Prof. Dr. Reiner ; Barthe, Prof. Dr. Gilles
Publikationsjahr: 2020
Ort: Darmstadt
Datum der mündlichen Prüfung: 8 Mai 2020
DOI: 10.25534/tuprints-00008540
URL / URN: https://tuprints.ulb.tu-darmstadt.de/8540
Kurzbeschreibung (Abstract):

Abstract programs contain schematic placeholders representing potentially infinitely many concrete programs. They naturally occur in multiple areas of computer science concerned with correctness: rule-based compilation and optimization, code refactoring and other source-to-source transformations, program synthesis, Correctness-by-Construction, and more. Mechanized correctness arguments about abstract programs are frequently conducted in interactive environments. While this permits expressing arbitrary properties quantifying over programs, substantial effort has to be invested to prove them manually by writing proof scripts. Existing approaches to proving abstract program properties automatically, on the other hand, lack expressiveness. Frequently, they only support placeholders representing all possible instantiations; in some cases, minor refinements are supported.

This thesis bridges that gap by presenting Abstract Execution (AE), an automatic reasoning technique for universal behavioral properties of abstract programs. The restriction to universal (no existential quantification) and behavioral (not addressing internal structure) properties excludes certain applications; however, it is the key to automation. Our logic for Abstract Execution uses abstract state changes to represent unknown effects on local variables and the heap, and models abrupt completion by symbolic branching. In this logic, schematic placeholders have names: It is possible to re-use them at several places, representing the same program elements in potentially different contexts. Furthermore, the represented concrete programs can be constrained by an expressive specification language, which is a unique feature of AE. We use the theory of dynamic frames to scale between full abstraction and total precision of frame specifications, and support fine-grained pre- and postconditions for (abrupt) completion.

We implemented AE by extending the program verifier KeY. Specifically for relational verification of abstract Java programs, we developed REFINITY, a graphical KeY frontend. We used REFINITY it in our signature application of AE: to model well-known statement-level refactoring techniques and prove their conditional safety. Several yet undocumented behavioral preconditions for safe refactorings originated in this case study, which is one of very few attempts to statically prove behavioral correctness of statement-level refactorings, and the only one to cover them to that extent.

AE extends Symbolic Execution (SE) for abstract programs. As a foundational contribution, we propose a general framework for SE based on the semantics of symbolic states. It natively integrates state merging by supporting m-to-n transitions. We define two orthogonal correctness notions, exhaustiveness and precision, and formally prove their relation to program proving and bug detection.

Finally, we introduce Modal Trace Logic (MTL), a trace-based logic to represent a variety of different program verification tasks, especially for relational verification. It is a “plug-in” logic which can be integrated on-demand with formal languages that have a trace semantics. The core of MTL is the trace modality, which allows expressing that a specification approximates an implementation after a trace abstraction step. We demonstrate the versatility of this approach by formalizing concrete verification tasks in MTL, ranging from functional verification over program synthesis to program evolution. To reason about MTL problems, we translate them to symbolic traces. We suggest Symbolic Trace Logic (STL), which comes with a sequent calculus to prove symbolic trace inclusions. This requires checking symbolic states for subsumption; to that end, we provide two generally useful notions of symbolic state subsumption. This framework relates as follows to the other parts of this thesis: We use the language of abstract programs to express synthesis and compilation, which connects MTL to AE. Moreover, symbolic states of STL are based on our framework for SE.

Alternatives oder übersetztes Abstract:
Alternatives AbstractSprache

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.

Deutsch
URN: urn:nbn:de:tuda-tuprints-85409
Sachgruppe der Dewey Dezimalklassifikatin (DDC): 000 Allgemeines, Informatik, Informationswissenschaft > 004 Informatik
Fachbereich(e)/-gebiet(e): 20 Fachbereich Informatik
20 Fachbereich Informatik > Software Engineering
Hinterlegungsdatum: 18 Jun 2020 10:49
Letzte Änderung: 24 Jun 2020 08:01
PPN:
Referenten: Hähnle, Prof. Dr. Reiner ; Barthe, Prof. Dr. Gilles
Datum der mündlichen Prüfung / Verteidigung / mdl. Prüfung: 8 Mai 2020
Export:
Suche nach Titel in: TUfind oder in Google
Frage zum Eintrag Frage zum Eintrag

Optionen (nur für Redakteure)
Redaktionelle Details anzeigen Redaktionelle Details anzeigen