@article { 135, title = {A Framework for Decision Procedures in Program Verification}, journal = {Formal Aspects of Computing}, volume = {21}, year = {2009}, month = {10/2009}, pages = {10}, publisher = {Springer}, chapter = {485}, abstract = {

We present a unifying framework for understanding and developing SAT-based decision procedures for Satisfiability Modulo Theories (SMT). The framework is based on a reduction of the decision problem to propositional logic by means of a deductive system. The two commonly used techniques, eager encodings (a direct reduction to propositional logic) and lazy encodings (a family of techniques based on an interplay between a SAT solver and a decision procedure) are identified as special cases. This framework offers the first generic approach for eager encodings, and a simple generalization of various lazy techniques that are found in the literature.


}, URL = {http://www.springerlink.com/content/fq8hq84307727483/}, author = {Kroening, Daniel and Strichman, Ofer} }