Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Back to the Future: Revisiting Precise Program Verification using SMT Solvers

Shuvendu Lahiri and Shaz Qadeer

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.

Details

Publication typeInproceedings
Published inPrinciples of Programming Languages (POPL '08)
Pages16
NumberMSR-TR-2007-88
InstitutionMicrosoft Research
PublisherAssociation for Computing Machinery, Inc.
> Publications > Back to the Future: Revisiting Precise Program Verification using SMT Solvers