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 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
- 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
- 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