Mechanised verification patterns for Dafny

Gudmund Grov; Yuhui Lin; Vytautas Tumas

doi:10.1007/978-3-319-48989-6_20

Mechanised verification patterns for Dafny

Gudmund Grov^*, Yuhui Lin, Vytautas Tumas

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

1 Citation (Scopus)

Abstract

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 language	English
Title of host publication	FM 2016
Subtitle of host publication	Formal Methods
Editors	John Fitzgerald, Constance Heitmeyer, Stefania Gnesi, Anna Philippou
Publisher	Springer
Pages	326-343
Number of pages	18
ISBN (Electronic)	9783319489896
ISBN (Print)	9783319489889
DOIs	https://doi.org/10.1007/978-3-319-48989-6_20
Publication status	Published - 2016
Event	21st International Symposium on Formal Methods 2016 - Limassol, Cyprus Duration: 9 Nov 2016 → 11 Nov 2016

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	9995
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	21st International Symposium on Formal Methods 2016
Country/Territory	Cyprus
City	Limassol
Period	9/11/16 → 11/11/16

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/978-3-319-48989-6_20

Cite this

@inproceedings{ff9dd8c1dc09449c821c2b343f566993,

title = "Mechanised verification patterns for Dafny",

abstract = "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.",

author = "Gudmund Grov and Yuhui Lin and Vytautas Tumas",

year = "2016",

doi = "10.1007/978-3-319-48989-6_20",

language = "English",

isbn = "9783319489889",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "326--343",

editor = "John Fitzgerald and Constance Heitmeyer and Stefania Gnesi and Anna Philippou",

booktitle = "FM 2016",

note = "21st International Symposium on Formal Methods 2016 ; Conference date: 09-11-2016 Through 11-11-2016",

}

TY - GEN

T1 - Mechanised verification patterns for Dafny

AU - Grov, Gudmund

AU - Lin, Yuhui

AU - Tumas, Vytautas

PY - 2016

Y1 - 2016

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84996551395&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-48989-6_20

DO - 10.1007/978-3-319-48989-6_20

M3 - Conference contribution

AN - SCOPUS:84996551395

SN - 9783319489889

T3 - Lecture Notes in Computer Science

SP - 326

EP - 343

BT - FM 2016

A2 - Fitzgerald, John

A2 - Heitmeyer, Constance

A2 - Gnesi, Stefania

A2 - Philippou, Anna

PB - Springer

T2 - 21st International Symposium on Formal Methods 2016

Y2 - 9 November 2016 through 11 November 2016

ER -

Mechanised verification patterns for Dafny

Abstract

Publication series

Conference

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this