Stp

Jul 20, 2023

Decision Procedure for Bitvectors and Arrays

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.



Checkout these related ports:
  • Zn_poly - C library for polynomial arithmetic
  • Zimpl - Language to translate the LP models into .lp or .mps
  • Zegrapher - Software for plotting mathematical objects
  • Zarray - Dynamically typed N-D expression system based on xtensor
  • Z3 - Z3 Theorem Prover
  • Yices - SMT solver
  • Yacas - Yet Another Computer Algebra System
  • Xtensor - Multi-dimensional arrays with broadcasting and lazy computing
  • Xtensor-python - Python bindings for xtensor
  • Xtensor-io - Xtensor plugin to read/write images, audio files, numpy npz and HDF5
  • Xtensor-blas - BLAS extension to xtensor
  • Xspread - Spreadsheet program for X and terminals
  • Xppaut - Graphical tool for solving differential equations, etc
  • Xplot - X11 plotting package
  • Xlife++ - XLiFE++ eXtended Library of Finite Elements in C++