index.html

---
layout: sidebar
---
<h2>The Simple Theorem Prover</h2>
<p>
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.
</p>

<h2>Features</h2>
<ul>
  <li>Easy to embed or run standalone</li>
  <li>Bindings for C, C++, and Python</li>
  <li>Supports multiple query input formats</li>
  <li>Open source and MIT licensed</li>
</ul>

<h2>Awards</h2>

<p>STP's speed and accuracy compare favorably with other solvers in the bitvector (QF_BV) category.</p>

<ul class="fa-ul">
  <li>
    <span class="fa-li"><i class="fas fa-trophy"></i></span>
    1st Single Query &mdash; SMTCOMP 2023
  </li>

  <li>
    <span class="fa-li"><i class="fas fa-trophy"></i></span>
    1st Single Query UNSAT &amp; Single Query 24sec Performance &mdash; SMTCOMP 2022
  </li>
  <li>
    <span class="fa-li"><i class="fas fa-trophy"></i></span>
    1st Cloud &amp; Incremental &mdash; SMTCOMP 2021
  </li>
  <li>
    <span class="fa-li"><i class="fas fa-trophy"></i></span>
    2nd &mdash; SMTCOMP 2014
  </li>
  <li>
    <span class="fa-li"><i class="fas fa-trophy"></i></span>
    2nd &mdash; SMTCOMP 2011
  </li>
  <li>
    <span class="fa-li"><i class="fas fa-trophy"></i></span>
    1st &mdash; SMTCOMP 2010
  </li>
  <li>
    <span class="fa-li"><i class="fas fa-trophy"></i></span>
    1st &mdash; SMTCOMP 2006
  </li>
</ul>