Conference Publication Details
Mandatory Fields
Leino K.;Monahan R.
Proceedings of the ACM Symposium on Applied Computing
Reasoning about comprehensions with first-order SMT solvers
Optional Fields
Matching triggers Quantifiers SMT solvers Spec#
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. Copyright 2009 ACM.
Grant Details