UCLID (/ˈjuːklɪd/, the same as "Euclid") is a decision procedure for CLU logic and can be used as a tool for bounded model checking of infinite-state systems.
Contents
Decision procedure and verification tool
UCLID is a tool for verifying models of computer systems. It started out primarily focused on infinite-state systems (i.e., systems that, in addition to Boolean state variables, have state variables that are integer-valued or functions from integers to integers or Booleans), but now is equipped with techniques to also reason about word-level descriptions of systems (those with finite-precision types). The key component of UCLID is a decision procedure for a decidable fragment of first-order logic, including uninterpreted functions and equality, integer linear arithmetic, finite-precision bit-vector arithmetic, and constrained lambda expressions (for modeling arrays, memories, etc.). The decision procedure operates by translating the input formula to an equi-satisfiable Boolean formula on which it invokes a Boolean satisfiability (SAT) solver.
Applications of UCLID include microprocessor verification, protocol analysis, analyzing software for security vulnerabilities, and verifying models of hybrid systems. The decision procedure can also be used as a stand-alone theorem prover, or within other first-order or higher-order logic theorem provers.
People
UCLID is a joint CMU – UC Berkeley project. The first version of UCLID was developed in Carnegie-Mellon University by Randal Bryant, Sanjit Seshia (now at UC Berkeley) and Shuvendu K. Lahiri (now at Microsoft Research).
Faculty
Students
Beaver – decision procedure for bit-vector arithmetic
Beaver bit-vector decision procedure is a new SMT solver (decision procedure) for the theory of quantifier-free finite-precision bit-vector arithmetic developed by the UCLID group at UC Berkeley as the next generation of UCLID's bit-vector decision procedure. It supports all operators defined under QF_BV. Beaver is specially adapted for the following applications — program analysis (SMT formulae rich in conjunction of linear constraints such as path feasibility queries), security (SMT formulae rich in nonlinear arithmetic) and equivalence checking (SMT formulae rich in Boolean structure).
Beaver is an eager decision procedure. Once the SAT problem is generated, any off-the-shelf SAT solver such as Minisat or Rsat can be used on the CNF formula. The main transformations performed by Beaver include:
- Constant propagation and constraint propagation using an event-driven approach.
- Number theoretic rewrite rules which exploit identities from finite ring algebra.
- Boolean synthesis for fast SAT solving using AIG as internal representation and ABC as logic synthesis engine.
Currently, it is a single pass compiler to Boolean satisfiability problem and it does not implement the proof based abstraction technique presented in Deciding Bit-Vector Arithmetic with Abstraction (TACAS, March 2007).
Beaver is implemented in OCaml and uses ABC library with an external SAT engine. It is an open-source software released under BSD. Beaver is available for download.