- Uclid
UCLID (pronounced IPA|/ˈjuklɪd/, the same as "Euclid") is a decision procedure for CLU logic and can be used as a tool for bounded
model checking ofinfinite-state systems.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 adecision procedure for a decidable fragment offirst-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 aBoolean satisfiability (SAT) solver.Applications of UCLID include
microprocessor verification,protocol analysis, analyzing software for security vulnerabilities, and verifying models ofhybrid systems . The decision procedure can also be used as a stand-alonetheorem 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
CMU by Randal Bryant, Sanjit Seshia (now atUC Berkeley ) and Shuvendu K. Lahiri (now atMicrosoft Research ).Current team consists of
Faculty
* Randal E. Bryant (CMU) [http://www.cs.cmu.edu/~bryant/]
* Sanjit A. Seshia (UC Berkeley) [http://www.eecs.berkeley.edu/~sseshia/]tudents
* Bryan A. Brady (UC Berkeley) [http://www.eecs.berkeley.edu/~bbrady/]
* Susmit Jha (UC Berkeley) [http://www.eecs.berkeley.edu/~jha/]
* Hormoz Zarnani (CMU)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:
1. Constant propagation and constraint propagation using an event-driven approach.
2. Number theoretic rewrite rules which exploit identities from finite ring algebra.
3. 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 at [http://www.eecs.berkeley.edu/~jha/beaver.html Beaver website] .
Recent Publications
2007
* Symbolic Reachability Analysis of Lazy Linear Hybrid Automata. Susmit Jha, Bryan Brady, and Sanjit A. Seshia. In 5th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS), October 2007
* On Solving Boolean Combinations of UTVPI Constraints. Sanjit A. Seshia, K. Subramani, and Randal E. Bryant. In Journal of Boolean Satisfiability, Modeling, and Computation (JSAT), 2007
* Deciding Bit-Vector Arithmetic with Abstraction. Randal E. Bryant, Daniel Kroening, Joel Ouaknine, Sanjit A. Seshia, Ofer Strichman, and Bryan Brady. In 13th Intl. Conference on Tools and Algorithms for the Construction of Systems (TACAS), pages 358-372, March 20072005
* Adaptive Eager Boolean Encoding for Arithmetic Reasoning in Verification. Sanjit A. Seshia. Ph.D. Thesis, Carnegie Mellon University, May 2005.
* Automatic Discovery of API-Level Exploits. Vinod Ganapathy, Sanjit A. Seshia, Somesh Jha, Thomas W. Reps, and Randal E. Bryant. 27th International Conference on Software Engineering (ICSE), 2005
* Semantics-Aware Malware Detection. Mihai Christodorescu, Somesh Jha, Sanjit A. Seshia, Dawn Song, and Randal E. Bryant. IEEE Symposium on Security and Privacy, Oakland, May 2005
* Term-Level Verification of a Pipelined CISC Microprocessor. Randal E. Bryant. Computer Science Department Technical Report CMU-CS-05-195, December 20052004
* The UCLID Decision Procedure. Shuvendu K. Lahiri and Sanjit A. Seshia. Proc. of Intl. Conf. on Computer-Aided Verification (CAV), LNCS 3114, pages 475-478, July 2004.
* Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds. Sanjit A. Seshia and Randal E. Bryant. Proc. of 19th Annual IEEE Symposium on Logic in Computer Science (LICS), pages 100-109, July 2004.
* Abstraction-based Satisfiability Solving of Presburger Arithmetic. Daniel Kroening, Joël Ouaknine, Sanjit A. Seshia, and Ofer Strichman. Proc. of Intl. Conf. on Computer-Aided Verification (CAV), LNCS 3114, pages 308-320, July 2004.2003
* Deciding Quantifier-Free Presburger Formulas Using Finite Instantiation Based on Parameterized Solution Bounds. Sanjit A. Seshia and Randal E. Bryant. Computer Science Department Technical report CMU-CS-03-210, December 2003.
* A Hybrid SAT-Based Decision Procedure for Separation Logic with Uninterpreted Functions. Sanjit A. Seshia, Shuvendu K. Lahiri, and Randal E. Bryant. In Proc. 40th Design Automation Conference (DAC), ACM Press, pages 425-430, June 2003.
* Convergence Testing in Term-Level Bounded Model Checking. Randal E. Bryant, Shuvendu K. Lahiri, and Sanjit A. Seshia. 12th Conference on Correct Hardware Design and Verification Methods (CHARME), LNCS 2860, pages 348-362, October 2003.
* Convergence Testing in Term-Level Bounded Model Checking. R. E. Bryant, S. K. Lahiri, and S. A. Seshia. Computer Science Department Technical report CMU-CS-03-156, June 2003.References
Sanjit's page at
UC Berkeley [http://www.eecs.berkeley.edu/~sseshia/research/uclid.html]UCLID
wiki [http://uclid.eecs.berkeley.edu/wiki/index.php/Main_Page]
Wikimedia Foundation. 2010.