MURAL - Maynooth University Research Archive Library



    Reasoning about Comprehensions with First-Order SMT Solvers


    Leino, K. Rustan M. and Monahan, Rosemary (2009) Reasoning about Comprehensions with First-Order SMT Solvers. In: SAC '09 Proceedings of the 2009 ACM symposium on Applied Computing. ACM, New York, pp. 615-622. ISBN 9781605581668

    [img] Download (211kB)


    Share your research

    Twitter Facebook LinkedIn GooglePlus Email more...



    Add this article to your Mendeley library


    Abstract

    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 off-the-shelf first-order SMT solvers. Since a first- order SMT solver does not directly support the bound variables that occur in comprehension expressions, the challenge is to provide a sound axiomatisation that is strong enough to prove interesting programs and, furthermore, that can be used automatically by the SMT solver. 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: Book Section
    Additional Information: © ACM, 2009. The final and definitive version of this article has been published in SAC '09 Proceedings of the 2009 ACM symposium on Applied Computing (ISBN 9781605581668) doi>10.1145/1529282.1529411
    Keywords: SMT Solvers; Matching Triggers; Quantiers; Spec#;
    Academic Unit: Faculty of Science and Engineering > Computer Science
    Item ID: 3932
    Depositing User: Rosemary Monahan
    Date Deposited: 09 Oct 2012 15:29
    Publisher: ACM
    Refereed: Yes
    URI:

    Repository Staff Only(login required)

    View Item Item control page

    Downloads

    Downloads per month over past year