Add README.md. Update %description.
This commit is contained in:
parent
3667802c8b
commit
b8386c3169
|
@ -0,0 +1,16 @@
|
|||
# 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/).
|
3
stp.spec
3
stp.spec
|
@ -41,8 +41,7 @@ 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 at:
|
||||
http://people.csail.mit.edu/vganesh/STP_files/stp.html
|
||||
Additional information can be found at https://stp.readthedocs.io/.
|
||||
|
||||
%package devel
|
||||
Summary: Development files for STP constraint solver/decision procedure
|
||||
|
|
Loading…
Reference in New Issue