0 Kroening, Daniel Strichman, Ofer 2009 A Framework for Decision Procedures in Program Verification Formal Aspects of Computing Springer 21 5 10 10/2009 <p><span class="Apple-style-span" style="color: rgb(0, 0, 37); font-family: Verdana, Helvetica, sans-serif; font-size: 14px; line-height: normal; -webkit-border-horizontal-spacing: 4px; -webkit-border-vertical-spacing: 4px; ">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,&nbsp;<i>eager</i>&nbsp;encodings (a direct reduction to propositional logic) and&nbsp;<i>lazy</i>&nbsp;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.</span></p><p>&nbsp;</p> http://www.springerlink.com/content/fq8hq84307727483/