TU Darmstadt / ULB / TUprints

Automating Type Soundness Proofs for Domain-Specific Languages

Grewe, Sylvia (2019)
Automating Type Soundness Proofs for Domain-Specific Languages.
Technische Universität Darmstadt
Ph.D. Thesis, Primary publication

[img]
Preview
Text
SylviaGreweDissertation.pdf - Published Version
Copyright Information: CC BY-SA 4.0 International - Creative Commons, Attribution ShareAlike.

Download (4MB) | Preview
Item Type: Ph.D. Thesis
Type of entry: Primary publication
Title: Automating Type Soundness Proofs for Domain-Specific Languages
Language: English
Referees: Mezini, Prof. Dr. Mira ; Kovács, Prof. Dr. Laura ; Erdweg, Prof. Dr. Sebastian
Date: 3 September 2019
Place of Publication: Darmstadt
Date of oral examination: 12 July 2019
Abstract:

Type systems for static programming languages are supposed to ensure the absence of type errors in code prior to execution. Type systems that meet this expectation are called sound type systems in the literature. In practice, however, many type systems are unsound, i.e. they successfully type-check programs with type errors which get stuck during execution due to undefined behavior.

To reliably ensure that a type system is sound, a sub-area in programming languages research proposes to develop type soundness proofs: One proves a soundness property for a logical specification of a type system via logical deduction. The mechanization of such a proof shall ensure the absence of human-made deduction errors within the different reasoning steps: A verification system checks that all steps within a proof a correct with regard to the rules within the used logic.

However, developing mechanized type soundness proofs with the tool support and methodologies available today is a cumbersome task even for verification experts: The available support often requires to spell out a large number of "trivial" steps within such proofs manually, which necessitates a certain level of skills and expertise in the area of mechanized verification. Often, language developers and researchers who are experts in conducting type soundness proofs on paper are not necessarily also well-versed in using tool support for mechanized verification. These developers and researchers are typically quickly frustrated by the effort required for mechanized verification and hence often do not attempt it.

The main goal of this thesis is to raise the degree of automation for mechanizing type soundness proofs. To this end, we first study existing mechanization efforts for type soundness proofs from the literature. We use our observations on the one hand to restrict the set of languages we consider in this thesis: We focus on domain-specific languages (DSLs) without first-class binders. On the other hand, we use our observations to identify general shortcomings of existing verification systems regarding how well they support experts in different verification domains in developing domain-specific, automated proof strategies for their domain.

Based on our observations, we propose a generic verification infrastructure called VeriTaS for the automation of domain-specific verification tasks: VeriTaS is a lightweight library in Scala for combining high-level automated domain-specific proof strategies with existing automated theorem provers for the verification of individual, low-level proof steps. VeriTaS is generic in a format for input specifications. Hence, the infrastructure may be instantiated for different verification domains.

We instantiate our VeriTaS verification infrastructure for generating type soundness proofs of DSLs: We provide a domain-specific input format for type system specifications and basic tactics for creating low-level proof steps. Furthermore, we present automated proof strategies that generate proof structures for type soundness proofs. We evaluate our proof strategies on two case studies, both type systems of representative DSLs. Also, we conduct an empirical study to compare different encoding strategies for low-level proof problems. We used the results of our empirical study to raise the degree of automation provided by our proof strategies for type soundness proofs of DSLs further.

Our case studies show that our instantiation of VeriTaS for type soundness proofs of DSLs achieves a higher degree of automation for such proofs than existing systems.

Alternative Abstract:
Alternative AbstractLanguage

Typsysteme für statische Programmiersprachen sollen die Abwesenheit von Typfehlern in Quellcode prüfen, bevor ein Programm ausgeführt wird. Typsysteme, die diese Erwartung erfüllen, werden in der Literatur als korrekte Typsysteme bezeichnet. In der Praxis sind viele Typsysteme allerdings nicht korrekt, d.h. sie akzeptieren unter Umständen Programme mit Typfehlern, die während der Ausführung zu undefiniertem Verhalten führen. Um verlässlich die Korrektheit eines Typsystems sicherzustellen schlägt ein Untergebiet in der Forschung zu Programmiersprachen vor, Korrektheitsbeweise von Typsystemen zu entwickeln: Man beweist formal eine Korrektheitseigenschaft für eine logische Spezifikation eines Typsystems mit Hilfe von logischen Schlussfolgerungen. Die Mechanisierung eines solchen Beweises soll sicherstellen, dass der Beweis keine menschengemachten Schlussfolgerungsfehler enthält: Ein Verifikationssystem überprüft, ob alle Schritte in einem Beweis korrekt im Hinblick auf die Regeln der verwendeten Logik sind.

Allerdings ist die Entwicklung von mechanisierten Korrektheitsbeweisen für Typsysteme mit Hilfe heutiger Methodik und heute verfügbaren Werkzeugen selbst für Experten im Bereich der formalen Verifikation eine äußerst aufwendige Aufgabe: Heute verfügbare Werkzeuge erfordern oft, dass eine große Anzahl "trivialer" Beweisschritte manuell ausformuliert werden, was ein gewisses Level an Fähigkeiten und Expertise im Gebiet der formalen Verifikation erfordert. Entwickler von Programmiersprachen sowie Forscher, die Experten darin sind, wie man Korrektheitsbeweise von Typsystemen auf dem Papier durchführt, sind oft nicht gleichzeitig versiert im Umgang mit Werkzeugen für mechanisierte Verifikation. Solche Entwickler und Forscher sind typischerweise schnell frustriert angesichts des nötigen Aufwands für mechanisierte Verifikation und verfolgen daher die Mechanisierung ihrer Beweise oft nicht weiter.

Das Hauptziel dieser Arbeit besteht darin, den Automatisierungsgrad für die Mechanisierung von Korrektheitsbeweisen für Typsysteme zu erhöhen. Hierfür studieren wir zunächst existierende Arbeiten zur Mechanisierung solcher Beweise aus der Literatur. Wir verwenden unsere Beobachtungen hierzu auf der einen Seite, um die Menge der Programmiersprachen, die wir in dieser Arbeit betrachten, einzuschränken: Wir beschränken uns auf domänenspezifische Programmiersprachen (DSLs) ohne vollwertige Konstrukte zum Binden von abstrakten Namen. Auf der anderen Seite verwenden wir unsere Beobachtungen um zu identifizieren, welche generellen Schwächen existierende Verifikationssysteme besitzen, wenn es darum geht, Experten in verschiedenen Verifikationsdomänen darin zu unterstützen, domänenspezifische, automatische Beweisstrategien innerhalb ihrer Domäne zu entwickeln.

Auf der Basis unserer Beobachtungen schlagen wir eine generische Verifikationsinfrastruktur namens VeriTaS für die Automatisierung von domänenspezifischen Verifikationsaufgaben vor: VeriTaS ist eine leichtgewichtige Programmierbibliothek in Scala um automatische, domänenspezifische Beweisstrategien für die Generierung von Hauptschritten von Beweisen mit existierenden automatischen Theorembeweisern zu kombinieren, welche einzelne, technische Beweisschritte verifizieren. VeriTaS ist generisch in einem Eingabeformat für Problemspezifikationen. Daher kann die Infrastruktur für verschiedene Verifikationsdomänen instanziiert werden.

Wir instanziieren unsere VeriTaS-Verifikationsinfrastruktur für die Generierung von Korrektheitsbeweisen für Typsysteme von DSLs: Wir stellen ein domänenspezifisches Eingabeformat für Typsystemspezifikationen sowie Basistaktiken bereit, welche einzelne detaillierte Beweisschritte erstellen. Außerdem präsentieren wir automatische Beweisstrategien zur Generierung von Beweisstrukturen für Korrektheitsbeweise von Typsysteme. Wir evaluieren unsere Beweisstrategien anhand von zwei Fallstudien, beides Typsysteme von repräsentativen DSLs. Zusätzlich führen wir eine empirische Studie durch, um verschiedene Enkodierungsstrategien für Beweisprobleme auf Detailebene miteinander zu vergleichen. Die Ergebnisse unserer Studie haben wir dazu verwendet, den Automatisierungsgrad unserer Beweisstrategien für Korrektheitsbeweise von Typsystemen in VeriTaS weiter zu erhöhen.

Unsere Fallstudien zeigen, dass unsere Instanziierung von VeriTaS für Korrektheitsbeweise von Typsystemen von DSLs einen höheren Automatisierungsgrad für solche Beweise erreicht als existierende Systeme.

German
URN: urn:nbn:de:tuda-tuprints-90255
Classification DDC: 000 Generalities, computers, information > 004 Computer science
Divisions: 20 Department of Computer Science > Software Technology
Date Deposited: 17 Sep 2019 12:34
Last Modified: 17 Sep 2019 12:34
URI: https://tuprints.ulb.tu-darmstadt.de/id/eprint/9025
PPN: 453893708
Export:
Actions (login required)
View Item View Item