@inproceedings{leino2009reasoning,
author = {Leino, Rustan and Monahan, Rosemary},
title = {Reasoning about Comprehensions with First-Order SMT Solvers},
booktitle = {SAC'09 March 8-12, 2009, Honolulu, Hawaii, U.S.A.},
year = {2009},
month = {March},
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.},
url = {http://approjects.co.za/?big=en-us/research/publication/reasoning-comprehensions-first-order-smt-solvers/},
edition = {SAC’09 March 8-12, 2009, Honolulu, Hawaii, U.S.A.},
}