@inproceedings{leino2007automatic,
author = {Leino, Rustan and Monahan, Rosemary},
title = {Automatic Verification of Textbook Programs that Use Comprehensions},
booktitle = {In FTfJP '07: Proceedings of the 9th Workshop on Formal Techniques for Java-like Programs},
year = {2007},
month = {January},
abstract = {Textbooks on program verification make use of simple programs in mathematical domains as illustrative examples. Mechanical verification tools can give students a quicker way to learn, because the feedback cycle can be reduced from days (waiting for hand-proofs to be graded by the teaching assistant) to seconds or minutes (waiting for the tool’s output). However, the mathematical domains that are so familiar to students (for example, sum-comprehensions) are not directly supported by first-order SMT solvers.

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 first-order SMT solvers. 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/automatic-verification-textbook-programs-use-comprehensions/},
edition = {In FTfJP ’07: Proceedings of the 9th Workshop on Formal Techniques for Java-like Programs},
}