/stp

Simple Theorem Prover.

Primary LanguageCOtherNOASSERTION

STP

STP is a constraint solver (or SMT solver) aimed at solving constraints of bitvectors and arrays. These types of constraints can be generated by program analysis tools, theorem provers, automated bug finders, cryptographic attack tools, intelligent fuzzers, model checkers, and by many other applications.

Homepage: http://stp.github.io/

Ubuntu PPA: https://launchpad.net/~simple-theorem-prover/+archive/ubuntu/ppa/+packages

Documentation: https://github.com/stp/stp/wiki

Build Status

Coverity Scan Build Status

Coverage Status

Build, install and test:

See the INSTALL file

Input format

The file based input formats that STP reads are the: CVC, SMT-LIB1, and SMT-LIB2 formats. The SMT-LIB2 format is the recommended file format, because it is parsed by all modern bitvector solvers. Only quantifier-free bitvectors and arrays are implemented from the SMTLibv2 format.

Usage

Fun use case, STP overflowing a 32b integer:

import stp
In [1]: import stp
In [2]: a = stp.Solver()
In [3]: x = a.bitvec('x')
In [4]: y = a.bitvec('y')
In [5]: a.add(x + y < 20)
In [6]: a.add(x  > 10)
In [7]: a.add(y  > 10)
In [8]: a.check()
Out[8]: True
In [9]: a.model()
Out[9]: {'x': 4294967287L, 'y': 11L}

Traditional use-case:

stp myproblem.smt

Architecture

The system performs word-level preprocessing followed by translation to SAT which is then solved by a SAT solver. In particular, we introduce several new heuristics for the preprocessing step, including abstraction-refinement in the context of arrays, a new bitvector linear arithmetic equation solver, and some interesting simplifications. These heuristics help us achieve several magnitudes of order performance over other tools, and also over straight-forward translation to SAT. STP has been heavily tested on thousands of examples sourced from various real-world applications such as program analysis and bug-finding tools like EXE, and equivalence checking tools and theorem-provers.

Authors

  • Vijay Ganesh
  • Trevor Hansen