UCLID: A Verification Tool for Infinite-State Systems

[ News | Download | Papers | Examples | Benchmarks | External Users | Contact ]


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 applications of UCLID explored to-date include microprocessor design verification, analyzing software for security exploits, and verifying distributed algorithms.

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


News

We will soon make a new release of UCLID with support for integer linear arithmetic and finite-precision bit-vector arithmetic. Suggestions for new features and other improvements are most welcome.

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

The current release is UCLID version 1.0. (Disclaimer, Copyright )

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:

The UCLID configuration script will need the location of some of these packages.The installation of UCLID and all its support packages will need about 40MB of free disk space. Note: The SAT checkers need not be installed before you install UCLID. However, we recommend installing atleast one SAT checker because, in our experience, Chaff and GRASP perform better than the MuDDy BDD package.

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


UCLID Papers and Documentation

The UCLID user manual is included in the distribution. You can also get it by clicking here (ps, pdf).

Here are some relevant publications:

    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.

     
    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.

     
    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.

     
    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.
    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.
More recent papers are available from here.

 

Example UCLID models

Here are some examples of UCLID specifications that are mentioned in our CAV'02 and FMCAD'02 papers:
  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

Here are tarred-gzipped files containing some benchmark formulas in different formats (as given below):

External Users and Collaborators

We are aware of UCLID users in the United States, Canada, Israel, India, and China. Here are publications by UCLID users that we know of: If you have used UCLID in your project, please let us know. If you have published papers based on your use of UCLID, please send us the citations of your papers.

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

We are very interested in getting feedback from users. Please email us comments and bug-reports.
In a bug-report, please report the following information:
1. The specification file
2. The output generated, including any error messages
3. The hardware and software platforms the run was made on
4. Any other helpful information you can provide

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

The UCLID tool has been implemented by  Shuvendu Lahiri and Sanjit Seshia



Email Shuvendu and Sanjit at sanjit+uclid@cs.cmu.edu
Last modified: Thu Dec 30 03:19:25 EST 2004

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