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


    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
    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 per month over past year

    Origin of downloads