%0 Journal Article %J Formal Aspects of Computing %D 2009 %T A Framework for Decision Procedures in Program Verification %A Kroening, Daniel %A Strichman, Ofer %I Springer %N 5 %P 10 %U http://www.springerlink.com/content/fq8hq84307727483/ %V 21 %X

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.


%8 10/2009