Vijay's HomePage

STP Main Page

STP Papers

Tools Using STP

STP
Documentation

STP Talk

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

We are currently adding the theory of finite sets and the theory of uninterpreted functions to STP.

Download STP source

• STP source at sourceforge.net 

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

Download STP wrappers

• 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
  

• The c_interface.h file
• The c_interface testcases file

STP Paper

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

STP Examples

• These examples (in CVCL format) were used for the CAV 2007 paper
• These examples (in CVCL format) are all the big array examples that we have collected so far from atleast 5 different applications

Lead Author and Project Leader

Other Contributors

Mike Katelman, PhD Candidate, University of Illinois, Urbana-Champaign

Trevor Alexander Hansen, PhD Candidate, University of Melbourne, Australia

Professor David Dill, Stanford University