SMT solvers [3,4] (Satisfiability-Modulo-Theories Solvers) are computer programs that decide the satis-fiability problem for rich logics such as the theory of bit-vectors and arrays [10], integers, and datatypes. SMT solvers have recently proven to be particularly useful in finding security vulnerabilities, debug-ging, and program analysis aimed at security. The reason for the success of SMT solvers are threefold: 1) The input logic of SMT solvers is rich enough to capture a wide variety of program behavior eas-ily and compactly, 2) SMT solvers have become very efficient at solving such formulas obtained from real-world applications, and 3) there are very effective techniques now available, such as symbolic exe-cution [7, 8, 11], that convert computation into SMT formulas. My solvers, STP [10] and HAMPI [12], are specifically designed to support computer security applications that perform security analysis aimed at finding security vulnerabilities [14], detecting malware [15] and constructing exploits [2, 6].
http://arxiv.org/abs/1204.2989
