Farrell, Marie and Reynolds, Conor and Monahan, Rosemary (2021) Using dafny to solve the VerifyThis 2021 challenges. In: International Workshop on Formal Techniques for Java-like Programs, July 13, Denmark.

Preview

Download (125kB) | Preview

Abstract

This paper provides an experience report of using the Dafny pro- gram verifier, at the VerifyThis 2021 program verification competi- tion. The competition aims to evaluate the usability of logic-based program verification tools in a controlled experiment, challenging both the verification tools and the users of those tools. We present the two challenges that we tackled during the competition and discuss our solutions. As a result, we identify strengths and weak- nesses of Dafny in the verification of relatively complex algorithms, and report on our experience of applying Dafny in this setting.

Item Type:	Conference or Workshop Item (Paper)
Keywords:	Deductive Verification; VerifyThis; Dafny; Verification Challenges;
Academic Unit:	Faculty of Science and Engineering > Computer Science
Item ID:	15431
Depositing User:	Rosemary Monahan
Date Deposited:	08 Feb 2022 12:59
Refereed:	No
URI:	Publisher
Use Licence:	This item is available under a Creative Commons Attribution Non Commercial Share Alike Licence (CC BY-NC-SA). Details of this licence are available here

Repository Staff Only(login required)

Item control page

Downloads

Origin of downloads