Beaver swMATH ID: 71 Software Authors: Sanjit Seshia Description: 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). Homepage: http://uclid.eecs.berkeley.edu/jha/beaver-dist/beaver.html Keywords: SMT solver; theorem prover; bit-vector arithmetic Related Software: Yices; z3; CVC4; MathSAT; Boolector; MiniSat; SMT-LIB; STP; MathSAT5; OpenSMT; cvc3; Chaff; MedleySolver; MachSMT; SATzilla; KLEE; Daikon; WoLFram; FOCI; Mcmt Cited in: 9 Publications all top 5 Cited by 31 Authors 1 Aiken, Alex 1 Bansal, Sorav 1 Bardin, Sébastien 1 Barrett, Clark W. 1 Biere, Armin 1 Carmona, Josep 1 Chakraborty, Supratik 1 Chhatani, Dinesh 1 Dillig, Isil 1 Dillig, Thomas 1 Gajavelly, Rajkumar 1 Gupta, Shubhani 1 Haldankar, Tanmay 1 Herrmann, Philippe 1 Heule, Marijn J. H. 1 Inala, Jeevana Priya 1 Järvisalo, Matti 1 Khasidashvili, Zurab O. 1 Mahajan, Anmol 1 Mistry, Rakesh 1 Mora, Federico 1 Perroud, Florian 1 Pimpalkhare, Nikhil 1 Polgreen, Elizabeth 1 Saxena, Aseem 1 Seger, Carl-Johan H. 1 Seshia, Sanjit Arunkumar 1 Singh, Rohit R. 1 Solar-Lezama, Armando 1 Solé, Marc 1 Tinelli, Cesare Cited in 2 Serials 1 Journal of Automated Reasoning 1 Formal Methods in System Design Cited in 3 Fields 9 Computer science (68-XX) 2 Mathematical logic and foundations (03-XX) 1 Information and communication theory, circuits (94-XX) Citations by Year