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.
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: |
|
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 per month over past year
Origin of downloads