Provided by: Cornell University
Date Added: Apr 2012
In the past several years, the author have written two SMT solvers called STP and HAMPI that have found widespread use in computer security research by leading groups in academia, industry and the government. In this paper, the author summarize the features of STP/HAMPI that make them particularly suited for computer security research, and a brief description of some of the more important projects that use them.SMT solvers (Satisfiability-Modulo-Theories Solvers) are computer programs that decide the satisfiability problem for rich logics such as the theory of bit-vectors and arrays, integers, and datatypes. SMT solvers have recently proven to be particularly useful in finding security vulnerabilities, debugging, and program analysis aimed at security.