Back to the Future: Revisiting Precise Program Verification using SMT Solvers

Principles of Programming Languages (POPL) |

Published by Association for Computing Machinery, Inc. | Organized by ACM

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.