From b8386c3169cbefd39cba0de26c402eba489b5603 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Tue, 19 Jul 2022 15:32:26 -0600 Subject: [PATCH] Add README.md. Update %description. --- README.md | 16 ++++++++++++++++ stp.spec | 3 +-- 2 files changed, 17 insertions(+), 2 deletions(-) create mode 100644 README.md diff --git a/README.md b/README.md new file mode 100644 index 0000000..121b710 --- /dev/null +++ b/README.md @@ -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/). diff --git a/stp.spec b/stp.spec index bc2d37b..65bbbfa 100644 --- a/stp.spec +++ b/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