MURAL - Maynooth University Research Archive Library



    Automatic verification of textbook programs that use comprehensions


    Leino, K. Rustan M. and Monahan, Rosemary (2007) Automatic verification of textbook programs that use comprehensions. In: Formal Techniques for Java-like Programs (FTfJP) ECOOP Workshop, July 30 - August 3 2007, Berlin. (Unpublished)

    [img] Download (135kB)


    Share your research

    Twitter Facebook LinkedIn GooglePlus Email more...



    Add this article to your Mendeley library


    Abstract

    Textbooks on program verification make use of simple programs in mathematical domains as illustrative examples. Mechanical verification tools can give students a quicker way to learn, because the feedback cycle can be reduced from days (waiting for hand-proofs to be graded by the teaching assistant) to seconds or minutes (waiting for the tool’s output). However, the mathematical domains that are so familiar to students (for example, sum-comprehensions) are not directly supported by first-order SMT solvers. This paper presents a technique for translating common comprehension expressions (sum, count , product , min, and max) into verification conditions that can be tackled by two first-order SMT solvers. The technique has been implemented in the Spec# program verifier. The paper also reports on the experience of using Spec# to verify several challenging programming examples drawn from a textbook by Dijkstra and Feijen.

    Item Type: Conference or Workshop Item (Paper)
    Keywords: program verification; mechanical verification tools; SMT solvers; Spec#; program verifier;
    Academic Unit: Faculty of Science and Engineering > Computer Science
    Item ID: 3935
    Depositing User: Rosemary Monahan
    Date Deposited: 09 Oct 2012 15:28
    Publisher: the authors
    Refereed: No
    URI:

    Repository Staff Only(login required)

    View Item Item control page

    Downloads

    Downloads per month over past year