| CARVIEW |
Select Language
HTTP/2 200
server: GitHub.com
content-type: text/html; charset=utf-8
last-modified: Mon, 22 Jan 2024 22:49:54 GMT
access-control-allow-origin: *
etag: W/"65aef112-ed1"
expires: Wed, 14 Jan 2026 12:31:25 GMT
cache-control: max-age=600
content-encoding: gzip
x-proxy-cache: MISS
x-github-request-id: 67E2:145092:166C6B:19163F:69678A44
accept-ranges: bytes
age: 0
date: Wed, 14 Jan 2026 12:21:25 GMT
via: 1.1 varnish
x-served-by: cache-bom-vanm7210030-BOM
x-cache: MISS
x-cache-hits: 0
x-timer: S1768393285.994298,VS0,VE204
vary: Accept-Encoding
x-fastly-request-id: 163ba80000cd7df1859aca938a15c91277f54b72
content-length: 1362
STP • The Simple Theorem Prover
The Simple Theorem Prover
STP is a constraint solver for the theory of quantifier-free bitvectors that can solve many kinds of problems generated by program analysis tools, theorem provers, automated bug finders, cryptographic algorithms, intelligent fuzzers and model checkers.
Features
- Easy to embed or run standalone
- Bindings for C, C++, and Python
- Supports multiple query input formats
- Open source and MIT licensed
Awards
STP's speed and accuracy compare favorably with other solvers in the bitvector (QF_BV) category.
- 1st Single Query — SMTCOMP 2023
- 1st Single Query UNSAT & Single Query 24sec Performance — SMTCOMP 2022
- 1st Cloud & Incremental — SMTCOMP 2021
- 2nd — SMTCOMP 2014
- 2nd — SMTCOMP 2011
- 1st — SMTCOMP 2010
- 1st — SMTCOMP 2006