17 lines
886 B
Markdown
17 lines
886 B
Markdown
|
# stp
|
||
|
|
|
||
|
|
[STP](http://stp.github.io/) (Simple Theorem Prover) 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, as well as companies and 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.
|
||
|
|
|
||
|
|
Additional information can be found [here](https://stp.readthedocs.io/).
|