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, Apple, etc.
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. STP can tell if the input formula is satisfiable or not and if is, then it can also generate a variable
assignment to satisfy the input formula. This output can then be used as the input to trigger a bug in a program or an input to trigger a fault in the VHDL system.
The initial versions of STP were written by Vijay Ganesh as part of his PhD thesis. The current primary maintainers are Mate Soos, Dan Liew, and Ryan Govostes. From the very beginning STP was expressly designed for symbolic-execution based analysis and testing. STP is based on the following papers:
- 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
- EXE: Automatically Generating Inputs of Death by Cristian Cadar, Vijay Ganesh, Peter Pawlowski, Dawson Engler, David Dill. In Proceedings of ACM Conference on Computer and Communications Security 2006 (CCS 2006), Alexandria, Virginia, October, 2006
The code is available on GitHub. Building the source from the tree should always work.
If you have any issue building or using the system, please file an issue at the GitHub repository. User group on google groups
- Project Founder: Dr. Vijay Ganesh, Assistant Professor, University of Waterloo, Ontario, Canada
- Trevor Hansen, PhD Student, University of Melbourne, Australia
- Maintainers: Ryan Govostes, Dan Liew, Mate Soos
Past contributors: Khoo Yit Phang, Ed Schwartz, 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). Please
note that everyone working on the project is doing so out of hobby or
as a way to help them in their work/study projects. Response times are
pretty short but some delay is expected. Issues do get resolved but
given the complexity of the system, it can take a while.
The STP constraint solver was written by Vijay Ganesh mostly in 2005 and 2006 as part of his PhD thesis work at Stanford University under the supervision of Professor David L. Dill.
Right from the start, the design of STP was aimed primarily at symbolic-execution based analysis and testing.
Development froze in the second half of 2007 and most of 2008/2009.
There was brief spurt of activity when Mike Katelman (University of
Illinois, Urbana-Champaign) worked on the clausal normal form generation
phase of STP while at NVIDIA during the summer of 2008. In spring of
2009 Trevor Hansen (University of Melbourne, Australia) took it upon
himself to clean up parts of STP code, especially the SMTLIB parser.
Vijay restarted work on STP in late summer/fall of 2009, aiming the
solver at bio and crypto problems, and continued maintaining the code until 2012. From 2006-2012, STP won the SMTCOMP (bit-vectors category) in 2006/2010, and placed second in 2011. It also became a solver of choice for many applications, particularly for symbolic-execution based analysis and testing.
In 2012-2013, a group of programmers (Ryan Govostes, Dan Liew, and Mate Soos) took it upon themselves to breathe new life into the project. They improved the performance dramatically, and STP placed second in the SMTCOMP (bit-vectors) 2014.