| Popis: |
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. |
