MURAL - Maynooth University Research Archive Library



    Using dafny to solve the VerifyThis 2021 challenges


    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.

    [img]
    Preview
    Download (125kB) | Preview


    Share your research

    Twitter Facebook LinkedIn GooglePlus Email more...



    Add this article to your Mendeley library


    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)

    View Item Item control page

    Downloads

    Downloads per month over past year

    Origin of downloads