Beaver: Engineering an efficient SMT solver for bit-vector arithmetic Beaver is an SMT solver (theorem prover) for the theory of quantifier-free finite-precision bit-vector arithmetic. It supports all operators defined under QF_BV, including signed and unsigned non-linear arithmetic operators. Beaver is specially adapted for solving SMT formulae arising out of program analysis (rich in conjunction of linear constraints such as path feasibility queries), security (rich in nonlinear arithmetic) and equivalence checking (rich Boolean structure).
Keywords for this software
References in zbMATH (referenced in 7 articles )
Showing results 1 to 7 of 7.
- Chakraborty, Supratik; Khasidashvili, Zurab; Seger, Carl-Johan H.; Gajavelly, Rajkumar; Haldankar, Tanmay; Chhatani, Dinesh; Mistry, Rakesh: Symbolic trajectory evaluation for word-level verification: theory and implementation (2017)
- Inala, Jeevana Priya; Singh, Rohit; Solar-Lezama, Armando: Synthesis of domain specific CNF encoders for bit-vector solvers (2016)
- Järvisalo, Matti; Biere, Armin; Heule, Marijn J. H.: Simulating circuit-level simplifications on CNF (2012)
- Solé, Marc; Carmona, Josep: An SMT-based discovery algorithm for C-nets (2012)
- Bardin, Sébastien; Herrmann, Philippe; Perroud, Florian: An alternative to SAT-based approaches for bit-vectors (2010)
- Dillig, Isil; Dillig, Thomas; Aiken, Alex: Small formulas for large programs: on-line constraint simplification in scalable static analysis (2010)
- Jha, Susmit; Limaye, Rhishikesh; Seshia, Sanjit A.: Beaver: engineering an efficient SMT solver for bit-vector arithmetic (2009) ioport