Making Whiley Boogie!

Mark Utting; David J Pearce; Lindsay Groves

doi:10.1007/978-3-319-66845-1_5

Back

Conference paper

Open access

Peer reviewed

Making Whiley Boogie!

Mark Utting, David J Pearce and Lindsay Groves

Integrated Formal Methods, pp.69-84

International Conference on Integrated Formal Methods (IFM), 13th (Turin, Italy, 20-Sep-2017–22-Sep-2017)

Lecture Notes in Computer Science (LNCS), 10510, Springer International Publishing

2017

DOI: https://doi.org/10.1007/978-3-319-66845-1_5

Files and links (3)

pdf

PDF - Author's Accepted Version197.59 kBDownload View

Accepted VersionPDF - Author Accepted Version Open Access

pdf

PDF - Presentation7.15 MBDownload View

PresentationPDF - Presentation Open Access

url

https://doi.org/10.1007/978-3-319-66845-1_5View

Published Version

Abstract

Whiley

Boogie

verifying compiler

intermediate verification language

semantic translation

impedance mismatch

The quest to develop increasingly sophisticated verification systems continues unabated. Tools such as Dafny, Spec#, ESC/Java, SPARK Ada, and Whiley attempt to seamlessly integrate specification and verification into a programming language, in a similar way to type checking. A common integration approach is to generate verification conditions that are handed off to an automated theorem prover. This provides a nice separation of concerns, and allows different theorem provers to be used interchangeably. However, generating verification conditions is still a difficult undertaking and the use of more "high-level" intermediate verification languages has become common-place. In particular, Boogie provides a widely used and understood intermediate verification language. A common difficulty is the potential for an impedance mismatch between the source language and the intermediate verification language. In this paper, we explore the use of Boogie as an intermediate verification language for verifying programs in Whiley. This is noteworthy because the Whiley language has (amongst other things) a rich type system with considerable potential for an impedance mismatch. We report that, whilst a naive translation to Boogie is unsatisfactory, a more abstract encoding is surprisingly effective.

Details

Title: Making Whiley Boogie!
Authors: Mark Utting (Author) - University of the Sunshine Coast - Faculty of Arts, Business and Law
David J Pearce (Author) - Victoria University of Wellington, New Zealand
Lindsay Groves (Author) - Victoria University of Wellington, New Zealand
Contributors: Nadia Polikarpova (Editor)
Steve Schneider (Editor)
Publication details: Integrated Formal Methods, pp.69-84
Conference details: International Conference on Integrated Formal Methods (IFM), 13th (Turin, Italy, 20-Sep-2017–22-Sep-2017)
Series: Lecture Notes in Computer Science (LNCS); 10510
Publisher: Springer International Publishing
Date published: 2017
DOI: 10.1007/978-3-319-66845-1_5
ISSN: 0302-9743; 0302-9743
Copyright note: Copyright © 2017 The Authors. The author's accepted verion is reproduced here in accordance with the publisher's copyright policy. The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-319-66845-1_5
Organisation Unit: School of Science and Engineering - Legacy; University of the Sunshine Coast, Queensland
Language: English
Record Identifier: 99450346102621
Output Type: Conference paper
Research Statement: false

Metrics

79 File views/ downloads

676 Record Views