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, Verilog etc.), 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

    • Download using SVN (subversion) by typing the following command on your xterm:
       svn co https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp stp


WARNING: PLEASE DO `ulimit -s unlimited` BEFORE RUNNING STP. OTHERWISE, THE YACC PARSER WILL SEGFAULT ON BIG EXAMPLES

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
  • STP ships native with Fedora

STP Paper

Authors

  • Project Leader and Founder - Dr. Vijay Ganesh, Assistant Professor, University of Waterloo, Ontario, Canada
  • Current Maintainers - Ryan Govostes, Khoo Yit Phang, Mate Soos (Security Researcher Labs), Ed Schwartz (CMU), Dan Liew

Past Significant Contributor

Other Past Contributor

  • Mike Katelman, PhD Student, University of Illinois, Urbana-Champaign, IL, USA
  • Philip Guo, Student, Stanford University, Stanford, CA, USA
  • David L. Dill, Professor, Stanford University, Stanford, CA, USA
  • Tim King, Student, Stanford University and NYU