A Decision Procedure for Bit-Vectors and Arrays

By Vijay Ganesh, David L. Dill. International Conference on Computer Aided Verification, 2007

702 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Computational Theory and Mathematics, Software

View Paper: https://www.semanticscholar.org/paper/580772507bca7b9a0318d251e13f5cd8fb028d7b

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Computational Theory and Mathematics

In Software

Citations in the corpus

HAMPI: a solver for string constraints (2009, methodology): “Fourth, if STP reports that the constraints are unsatis.able, then Hampi reports the same.”
cvc5: A Versatile and Industrial-Strength SMT Solver (2022, background): “Notable SMT solvers include Bitwuzla [92], Boolector [98], CVC4 [21], MathSAT [46], OpenSMT2 [72], SMTInterpol [44], SMT-RAT [50], STP [61], veriT [35], Yices2 [55], and Z3 [90].”
BAP: A Binary Analysis Platform (2011, unknown): “– Direct (API) and filesystem bindings to STP [7], as well as the ability to interact via the filesystem with SMTLIB1 compliant decision procedures.”
FloodGuard: A DoS Attack Prevention Extension in Software-Defined Networks (2015, methodology): “We modify the concolic execution engine in the NICE [11] project to implement our symbolic execution engine and use STP [17] as the path constraint solver.”
Stochastic superoptimization (2012, methodology): “Code sequences are converted into SMT formulae in the quantiﬁer free theory of bit-vector arithmetic used by the STP [8] theorem prover, and used to produce a query which asks whether both sequences produce the same side eﬀects on live outputs when executed from the same initial machine state.”
Symbolic execution for software testing in practice: preliminary assessment (2011, background): “As importantly, EXE provides the speed necessary to quickly solve the constraints generated by real code, through a combination of low-level optimizations implemented in its purposely designed constraint solver STP [13, 25], and a series of higher-level ones such as caching and irrelevant constraint”
ODR: output-deterministic replay for multicore debugging (2009, background): “Such constraints are desirable because the constraint solver we use can solve them in polynomial time [6].”
Handbook of Satisfiability (2021, background): “Bit-vectors provide a more compact representation and often allow problems to be solved more efficiently than if they were represented at the bit level [43, 38, 70].”
All You Ever Wanted to Know about Dynamic Taint Analysis and Forward Symbolic Execution (but Might Have Been Afraid to Ask) (2010, methodology): “For example, many application domains pass the generated formulas to a SMT solver [4, 32].”
BinHunt: Automatically Finding Semantic Differences in Binary Programs (2008, methodology): “The theorem prover we employ is STP [5].”
A Symbolic Execution Framework for JavaScript (2010, methodology): “The solver passes the constraints over this bit vector to a SMT (satisfiability modulo theories) decision procedure for the theory of bit vectors, STP [10] in our implementation.”
TaintScope: A Checksum-Aware Directed Fuzzing Tool for Automatic Software Vulnerability Detection (2010, methodology): “Thus, the complex constraint can be simplified to a simple one, which can be solved with current solvers such as STP [39].”