@inproceedings{lahiri2008back,
author = {Lahiri, Shuvendu and Qadeer, Shaz},
title = {Back to the Future: Revisiting Precise Program Verification using SMT Solvers},
organization = {ACM},
booktitle = {Principles of Programming Languages (POPL)},
year = {2008},
month = {January},
abstract = {This paper takes a fresh look at the problem of precise verification of heap-manipulating programs using first-order Satisfiability-Modulo-Theories (SMT) solvers. We augment the specification logic of such solvers by introducing the fullLogicName for specifying properties of heap-manipulating programs and a verifier for proving these properties. Our logic is expressive, closed under weakest preconditions, and efficiently implementable on top of existing SMT solvers. We have created a prototype implementation of our logic over the solvers Simplify and Z3 and used our prototype to verify many programs. Our preliminary experience is encouraging; the completeness and the efficiency of the decision procedure is clearly evident in practice and has greatly improved the user experience of the verifier.},
publisher = {Association for Computing Machinery, Inc.},
url = {http://approjects.co.za/?big=en-us/research/publication/back-to-the-future-revisiting-precise-program-verification-using-smt-solvers/},
pages = {16},
}