UCLID: A Verification Tool for Infinite-State Systems

UCLID (pronounced  "Euclid") is a tool for analyzing the correctness of models of hardware and software systems. UCLID can be used to model and verify infinite-state systems with variables of integer, Boolean, function, and array types. There are two main ways to use UCLID:

1. As a verifier, for term-level bounded model checking, correspondence checking, deductive verification, and predicate abstraction-based verification.
2. As a stand-alone decision procedure for the theories of uninterpreted functions and equality, integer linear arithmetic, and arrays. UCLID can also handle limited forms of quantification.

The people involved in theory and implementation of UCLID are Randal E. Bryant, Shuvendu K. Lahiri, and Sanjit A. Seshia.

NEWS

9/04.  A new variant of UCLID (called UCLID_PA) that uses predicate abstraction to verify UCLID models has been released. This tool implements the ideas of symbolic predicate abstraction and the indexed predicate abstraction.  It also contains the set of examples that were verified using predicate abstraction.

Download UCLID

We currently have a bytecode distribution, containing documentation, examples, and bytecode. [uclid_1_0_bc.tar.gz - size 406 KB expands to 1.2 MB]. Currently version 1.0 is only available for Linux (kernel 2.2.0 and higher versions -- Redhat 6.2 and higher). Installation instructions are in the README file. Version 1.0 uses Ofer Strichman's psep library.

We have discontinued distrbution of the old version 0.1.

UCLID is largely implemented in Moscow ML. To use UCLID, you will also need to download and install the following support software before installing UCLID:

• Moscow ML, version 2.00 or higher
• The Chaff SAT checker, mChaff and zChaff versions. Note that UCLID version 0.1 only works with mChaff.
• The GRASP SAT solver. It might be easier to install the binary than to compile from sources.
• The MuDDy BDD package, v1.7 or higher. Important: We recommend using MuDDy ver1.7, withthis patch.
• Perl version 5.0 or higher

If you are interested in changing the default settings of the decision procedure for the 1.0 version, look here.

UCLID Papers and Documentation

Here are some relevant publications:

• Modeling and Verifying Systems using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions.

Randal E. Bryant, Shuvendu K. Lahiri, and Sanjit A. Seshia.
In Proc. Computer-Aided Verification (CAV), July 2002.
This paper presents the CLU logic and describes a small-domain encoding based decision procedure used within UCLID.

 

• Deciding CLU Logic Formulas via Boolean and Pseudo-Boolean Encodings.

Randal E. Bryant, Shuvendu K. Lahiri, and Sanjit A. Seshia.
In Proc. Intl. Workshop on Constraints in Formal Verification ,September 2002. Associated with Intl. Conf. on Principles and Practice of Constraint Programming.
This paper describes three variants of a decision procedure for CLU and presents an empirical evaluation based on several benchmarks.

 

• Modeling and Verification of Out-of-order Microprocessors using UCLID.

Shuvendu K. Lahiri, Sanjit A. Seshia, and Randal E. Bryant.
In Proc. Intl. Conf. on Formal Methods in Computer-Aided Design (FMCAD), LNCS 2517, pages 142-159, November 2002.
This paper describes a case study and methodology of using UCLID for the modeling and verification of out-of-order processor designs.

 

• 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), pages 425-430, June 2003.
This paper describes an enhanced version of UCLID's decision procedure.

•  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), October 2003 (to appear).
This paper describes a method to detect convergence (fix-point) for bounded model checking of UCLID models. A new formal definition of convergence is presented and we present a sound translation to Quantified Separation Logic (QSL) to detect the convergence.

Example UCLID models

1. Out-of-order Execution Unit
2. DLX Pipelined Processor
3. Steven German's cache coherence protocol: Buggy version 1 and Buggy version 2

Benchmarks formulas generated from UCLID

• A set of Valid CLU logic formulas in Stanford Validity Checker (SVC) format (480 kB)
• A set of Unsatisfiable Boolean formulas in DIMACS Conjunctive Normal Form (CNF) format (16MB)
• A set of benchmarks for Pseudo-Boolean Constraint Solvers. All input formulas are unsatisfiable. A README file in the tarball describes the format. (20MB)

External Users and Collaborators

• Z. S. Andraus and K. A. Sakallah, Automatic Abstraction and Verification of Verilog Models, Proceedings of the Design Automation Conference (DAC), ACM/IEEE, 218-223, June, 2004.
• P. Manolios and S. K. Srinivasan. Automatic Verification of Safety and Liveness for XScale-Like Processor Models Using WEB Refinements, Proceedings of Design, Automation, and Test in Europe (DATE), 2004.

The UCLID project has greatly benefited from contributions from other researchers, both theoretical and implementation. Our collaborators include: Daniel Kroening, Joël Ouaknine, and Ofer Strichman.
 

Feedback

If you want to be on our mailing list, please send email to sanjit+ucllist@cs.cmu.edu with the subject line reading `Mailing list'.

Authors and Developers

This page has been accessed  times since May 18, 2001.
Counter courtesy of www.digits.com