Share and Export
Share and Export
Farrell, Marie, 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
3464971.3468422.pdf
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 |
| Related URLs: | |
| URI: | https://mural.maynoothuniversity.ie/id/eprint/15431 |
| 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
Downloads per month over past year
