Tactics for the Dafny Program Verifier

Gudmund Grov, Vytautas Tumas

Research output: Chapter in Book/Report/Conference proceedingConference contribution

4 Citations (Scopus)
115 Downloads (Pure)

Abstract

Many modern program verifiers are based on automated theorem provers, which enable full hiding of proof details and allow users to focus all their effort on the program text. This has the advantage that the additional expertise of theorem provers is not required, but has the drawback that when the prover fails to verify a valid program, the user has to annotate the program text with guidance for the verifier. This can be tedious, low-level and repetitive, and may impact on the annotation overhead, readability of the program text and overall development time. Inspired by proof tactics for interactive theorem provers , a notion of `tactics' for the state-of-the-art Dafny program verifier, called Tacny, is developed. With only minor extensions to the Dafny syntax, a user can encode high-level proof patterns as Dafny tactics, liberating herself from low-level and repetitive search tasks, whilst still working with familiar Dafny programming constructs. Manual search and guidance can be replaced with calls to such tactics, which will automate this task. We provide syntax and semantics for Tacny, and show feasibility through a prototype implementation, applied to several examples.
Original languageEnglish
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems
Subtitle of host publicationTACAS 2016
EditorsMarsha Chechik, Jean-François Raskin
PublisherSpringer
Pages36-53
Number of pages18
ISBN (Electronic)9783662496749
ISBN (Print)9783662496732
DOIs
Publication statusPublished - 9 Apr 2016
Event22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems 2016 - Eindhoven, Netherlands
Duration: 2 Apr 20168 Apr 2016

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume9636
ISSN (Print)0302-9743

Conference

Conference22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems 2016
Abbreviated titleTACAS 2016
CountryNetherlands
CityEindhoven
Period2/04/168/04/16

Fingerprint Dive into the research topics of 'Tactics for the Dafny Program Verifier'. Together they form a unique fingerprint.

  • Cite this

    Grov, G., & Tumas, V. (2016). Tactics for the Dafny Program Verifier. In M. Chechik, & J-F. Raskin (Eds.), Tools and Algorithms for the Construction and Analysis of Systems: TACAS 2016 (pp. 36-53). (Lecture Notes in Computer Science; Vol. 9636). Springer. https://doi.org/10.1007/978-3-662-49674-9_3