What is STP?

STP is a constraint solver (also referred to as a decision procedure or automated prover) aimed at solving constraints generated by program analysis tools, theorem provers, automated bug finders, biology, cryptography, intelligent fuzzers and model checkers. STP has been used in many research projects at Stanford, Berkeley, MIT, CMU and other universities. It is also being used at many companies such as NVIDIA, some startup companies, and by certain government agencies.

The input to STP are formulas over the theory of bit-vectors and arrays (This theory captures most expressions from languages like C/C++/Java and Verilog), and the output of STP is a single bit of information that indicates whether the formula is satisfiable or not. If the input is satisfiable, then it also generates a variable assignment to satisfy the input formula.

Download

• STP source at sourceforge.net
  

• Download using SVN (subversion) by typing the following command on your xterm:

Download STP wrappers and Ports

• Python Wrapper for STP written by Roberto Paleari from University of Milan, Italy. These bindings are released under GNU General Public License

• Ocaml Wrapper for STP written by Dawn Song's group at CMU and Berkeley. These bindings are released under the Stanford License

• Java Bindings for STP written by Adam Kiezun from MIT. These bindings are released under the MIT license
  

• STP has been ported to OpenBSD by Kevin Lo, and can be found at http://www.openbsd.org/cgi-bin/cvsweb/ports/devel/stp/ (STP can be installed via the ports tree)

• STP ships native with Fedora
  

STP Paper

• A Decision Procedure for Bit-vectors and Arrays by Vijay Ganesh and David L. Dill. In Proceedings of the International Conference in Computer Aided Verification (CAV 2007), Berlin, Germany, July 2007
  

Lead Author and Project Leader

Other Significant Contributor

• Trevor Alexander Hansen, PhD Student, University of Melbourne, Australia