Automating Proof Steps of Progress Proofs: Comparing Vampire and Dafny

Sylvia Grewe, Sebastian Erdweg, Mira Mezini

Research output: Chapter in Book/Conference proceedings/Edited volumeConference contributionScientificpeer-review

18 Downloads (Pure)


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 [3] project aims at providing support for the development of soundness proofs of type systems and efficient type checker implementations from type system specifications. 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 [13] and calls Vampire [8] on them, and secondly, the programming language Dafny [6], which translates proof goals and specifications to the intermediate verification language Boogie 2 [5] and calls the SMT solver Z3 [9] on them. We find that Vampire and Dafny are equally well-suited for automatically proving simple steps within progress proofs.
Original languageEnglish
Title of host publicationProceedings of the 3rd Vampire Workshop
EditorsLaura Kovacs, Andrei Voronkov
PublisherEPIC 2009
Number of pages13
Publication statusPublished - 2016
EventVampire 2016: 3rd Vampire Workshop - Coimbra, Portugal
Duration: 2 Jul 20162 Jul 2016

Publication series

NameEPIC Series in Computing
ISSN (Print)2398-7340


WorkshopVampire 2016

Fingerprint Dive into the research topics of 'Automating Proof Steps of Progress Proofs: Comparing Vampire and Dafny'. Together they form a unique fingerprint.

Cite this