Edinburgh Research Explorer

Mechanised Verification Patterns for Dafny

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

Original languageEnglish
Title of host publicationFM 2016: Formal Methods - 21st International Symposium, Limassol, Cyprus, November 9-11, 2016, Proceedings
PublisherSpringer, Cham
Pages326-343
Number of pages18
ISBN (Electronic)978-3-319-48989-6
ISBN (Print)978-3-319-48988-9
DOIs
StatePublished - 8 Nov 2016
Event21st International Symposium on Formal Methods - Limassol, Cyprus
Duration: 7 Nov 201611 Nov 2016
http://fm2016.cs.ucy.ac.cy/

Publication series

NameLecture Notes in Computer Science
PublisherSpringer, Cham
Volume9995
ISSN (Print)0302-9743

Conference

Conference21st International Symposium on Formal Methods
Abbreviated titleFM 2016
CountryCyprus
CityLimassol
Period7/11/1611/11/16
Internet address

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.

Event

21st International Symposium on Formal Methods

7/11/1611/11/16

Limassol, Cyprus

Event: Conference

Download statistics

No data available

ID: 41132901