Conference Publication Details
Mandatory Fields
Farrell M.;Reynolds C.;Monahan R.
FTfJP 2021 - Proceedings of the 23rd ACM International Workshop on Formal Techniques for Java-Like Programs, co-located with ECOOP/ISSTA 2021
Using dafny to solve the VerifyThis 2021 challenges
0 ()
Optional Fields
Dafny Deductive Verification Verification Challenges VerifyThis
This paper provides an experience report of using the Dafny program verifier, at the VerifyThis 2021 program verification competition. 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 weaknesses of Dafny in the verification of relatively complex algorithms, and report on our experience of applying Dafny in this setting.
Grant Details