The Simple Theorem Prover
STP is a constraint solver for the theory of quantifier-free bitvectors that can solve many kinds of problems generated by program analysis tools, theorem provers, automated bug finders, cryptographic algorithms, intelligent fuzzers and model checkers.
- Easy to embed or run standalone
- Bindings for C, C++, and Python
- Supports multiple query input formats
- Open source and MIT licensed
STP's speed and accuracy compare favorably with other solvers in the bitvector category.
- 2nd — SMTCOMP 2014
- 2nd — SMTCOMP 2011
- 1st — SMTCOMP 2010
- 1st — SMTCOMP 2006