Leino, K. Rustan M. and Monahan, Rosemary (2007) Automatic verification of textbook programs that use comprehensions. In: Formal Techniques for Java-like Programs (FTfJP) ECOOP Workshop, July 30 - August 3 2007, Berlin. (Unpublished)

Download (135kB)

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.

Item Type:	Conference or Workshop Item (Paper)
Keywords:	program verification; mechanical verification tools; SMT solvers; Spec#; program verifier;
Academic Unit:	Faculty of Science and Engineering > Computer Science
Item ID:	3935
Depositing User:	Rosemary Monahan
Date Deposited:	09 Oct 2012 15:28
Publisher:	the authors
Refereed:	No
URI:	http://ecoop07.swt.cs.tu-berlin.de/
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