This version of UCLID (called UCLID_PA to stand for UCLID with Predicate
Abstraction) supports the verification of UCLID models using predicate abstraction.
Unlike many other tools that use predicate abstraction, the present tool
supports two enhancements that improve the efficiency and automation of the
predicate abstraction process:

**Symbolic Predicate Abstraction:**Most previous implementations of predicate abstraction suffer from the need to make an exponentially large number of calls to construct the abstraction. This version uses a symbolic technique that uses Boolean methods to compute the abstraction symbolically. The key idea is to formulate the abstraction step symbolically and translate a quantified second-order formula to a quantified Boolean formula (that preserves certain properties) and use Boolean quantification based technique.**Indexed Predicate Abstraction:**For verifying systems with unbounded resources, one requires quantified invariants. Traditional use of predicate abstraction considered quantified predicates that can be extremely complex. We use "indexed" predicates, where the predicates contain free variables (e.g. pc(i) = Critical, where pc is a state variable, and i is a free variable in the predicate that refers to an arbitrary index of pc). This helps keep the predicates simple and improves automation in constructing quantified invariants.

This people involved in the theory and implementation of this tool are Shuvendu
K. Lahiri and Randal E. Bryant.

We currently have a bytecode distribution, containing examples, and
bytecode. [uclid_pa.v0_1.tar.gz
- size 1.5 MB expands to 6.0 MB]. Currently version 0.1 is only available
for Linux (kernel 2.4.20 and higher versions). Installation instructions
are in the README file.

- Version 0.1 uses Daniel Kroening's SATQE binary for performing quantifier elimination from an existentially quantified Boolean formula.
- It also uses a BDD-based cube compression algorithm implemented using Fabio Somenzi's CUDD package.

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

- Moscow ML, version 2.00 or higher
- The Chaff SAT checker, mChaff and zChaff versions. Note that the version 0.1 only works with mChaff.
- The GRASP SAT solver. It might be easier to install the binary than to compile from sources.
- Perl version 5.0 or higher

Here are some relevant publications:

"A Symbolic
Approach to Predicate Abstraction"

Shuvendu K. Lahiri, Randal
E. Bryant and Byron Cook.

*In Proc. of Computer-Aided Verification
(CAV 03), *

"Constructing
Quantified Invariants via Predicate Abstraction"

Shuvendu K. Lahiri and Randal E. Bryant

*In Proc. of 5th Intl. Conference on Verification,
Model Checking and Abstract Interpretation (VMCAI), **LNCS ** *2937*, Springer-Verlag, Pages 267-281,** Venice, Italy, January 2004.*

Shuvendu K. Lahiri, Randal E. Bryant

In Proc. of

The most updated version of the above papers can be found in the following Ph.D. thesis:

Shuvendu K. Lahiri.

Ph.D. Thesis

Last modified: Sun Sept 12 03:00:42 EDT 2004

*This page has been accessed
times since Sept 12, 2004.*

*Counter courtesy of www.digits.com*