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

Download (211kB)

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:	http://www.acm.org/
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)

Item control page

Downloads

Origin of downloads