Uclid

From Wikipedia, the free encyclopedia

UCLID (pronounced /ˈjuklɪd/, the same as "Euclid") is a tool for reasoning about the correctness of infinite-state systems.

Contents

[edit] 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.

[edit] People

UCLID is a joint CMU - UC Berkeley project. The first version of UCLID was developed in CMU by Randal Bryant, Sanjit Seshia (now at UC Berkeley) and Shuvendu K. Lahiri ( now at Microsoft Research).

Current team consists of

[edit] Faculty

  • Randal E. Bryant (CMU) [1]
  • Sanjit A. Seshia (UC Berkeley) [2]

[edit] Students

  • Bryan A. Brady (UC Berkeley) [3]
  • Susmit Jha (UC Berkeley) [4]
  • Hormoz Zarnani (CMU)

[edit] Recent Publications

[edit] 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 2007


[edit] 2005

  • 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 2005

[edit] 2004

  • 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.

[edit] 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.

[edit] References

Sanjit's page at UC Berkeley [5]

UCLID wiki [6]