| 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 22:36:52 GMT
cache-control: max-age=600
content-encoding: gzip
x-proxy-cache: MISS
x-github-request-id: 942E:3E283B:4DF8D:5AEE8:6968182C
accept-ranges: bytes
age: 0
date: Wed, 14 Jan 2026 22:26:53 GMT
via: 1.1 varnish
x-served-by: cache-bom-vanm7210083-BOM
x-cache: MISS
x-cache-hits: 0
x-timer: S1768429613.808443,VS0,VE212
vary: Accept-Encoding
x-fastly-request-id: 77b750bb7a37f1bdad197af9685cfa5bf922816a
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