Mechanised verification patterns for Dafny

Gudmund Grov*, Yuhui Lin, Vytautas Tumas

*Corresponding author for this work

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

1 Citation (Scopus)


In Dafny, the program text is used to both specify and implement programs in the same language [24]. It then uses a fully automated theorem prover to verify that the implementation satisfies the specification. However, the prover often needs further guidance from the user, and another role of the language is to provide such necessary hints and guidance. In this paper, we present a set of verification patterns to support this process. In previous work, we have developed a tactic language for Dafny, where users can encode their verification patterns and re-apply them for several proof tasks [16]. We extend this language with new features, implement our patterns in this tactic language and show, through experiments, generality of the patterns, and applicability of the tactic language.

Original languageEnglish
Title of host publicationFM 2016
Subtitle of host publicationFormal Methods
EditorsJohn Fitzgerald, Constance Heitmeyer, Stefania Gnesi, Anna Philippou
Number of pages18
ISBN (Electronic)9783319489896
ISBN (Print)9783319489889
Publication statusPublished - 2016
Event21st International Symposium on Formal Methods 2016 - Limassol, Cyprus
Duration: 9 Nov 201611 Nov 2016

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference21st International Symposium on Formal Methods 2016

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'Mechanised verification patterns for Dafny'. Together they form a unique fingerprint.

Cite this