KIT | KIT-Bibliothek | Impressum | Datenschutz

Automating Proof Steps of Progress Proofs: Comparing Vampire and Dafny

Grewe, Sylvia; Erdweg, Sebastian ORCID iD icon 1; Mezini, Mira
1 Institut für Programmstrukturen und Datenorganisation (IPD), Karlsruher Institut für Technologie (KIT)

Abstract (englisch):

Developing provably sound type systems is a non-trivial task which, as of today, typically requires expert skills in formal methods and a considerable amount of time. Our Veritas project aims at providing support for the development of soundness proofs of type systems and efficient type checker implementations from specifications of type systems. To this end, we investigate how to best automate typical steps within type soundness proofs.
In this paper, we focus on progress proofs for type systems of domain-specific languages. As a running example for such a type system, we model a subset SQL and augment it with a type system. We compare two different approaches for automating proof steps of the progress proofs for this type system against each other: firstly, our own tool Veritas, which translates proof goals and specifications automatically to TPTP and calls Vampire on them, and secondly, the programming language Dafny, which translates proof goals and specifications to the intermediate verification language Boogie 2 and calls the SMT solver Z3 on them. We find that Vampire and Dafny are equally well-suited for automatically proving simple steps within progress proofs.


Download
Originalveröffentlichung
DOI: 10.29007/5zjp
Dimensions
Zitationen: 5
Zugehörige Institution(en) am KIT Institut für Programmstrukturen und Datenorganisation (IPD)
Publikationstyp Proceedingsbeitrag
Publikationsjahr 2016
Sprache Englisch
Identifikator ISSN: 2398-7340
KITopen-ID: 1000188567
Erschienen in Proceedings of the 3rd Vampire Workshop; Coimbra, Portugal, 02.07.2016
Veranstaltung 3rd Vampire Workshop (2016), Coimbra, Portugal, 02.07.2016
Verlag EasyChair
Seiten S. 33-45
Serie EPiC Series in Computing ; 44
Nachgewiesen in Dimensions
OpenAlex
KIT – Die Universität in der Helmholtz-Gemeinschaft
KITopen Landing Page