UCLID: A Verification Tool for Infinite-State Systems

UCLID (pronounced  "Euclid") is a tool for verifying infinite-state systems. UCLID models systems using an arithmetic of counters, uninterpreted terms, and restricted lambda expressions. UCLID can be used in two ways:

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

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

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 that uses a Boolean encoding technique customized for each formula.
 

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

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