mirror of
https://git.FreeBSD.org/ports.git
synced 2024-11-30 01:15:52 +00:00
15 lines
885 B
Plaintext
15 lines
885 B
Plaintext
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, 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, some startup companies, and by certain 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.
|
|
|
|
WWW: http://people.csail.mit.edu/vganesh/STP_files/stp.html
|