UCLID_PA: Verification tool for UCLID models
using Predicate Abstraction
[ Download | Papers | Examples
| Contact ]
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.
Caution: Many of the features of the original UCLID distribution
(e.g. checking validity of formula, performing symbolic simulation) are
not present in this distribution. This version is solely meant to be used
for verifying systems using predicate abstraction. Future releases will
try to integrate this version with the main distribution.
This people involved in the theory and implementation of this tool are Shuvendu
K. Lahiri and Randal E. Bryant.
Download UCLID_PA
The current release
is UCLID_PA version 0.1. (Disclaimer, Copyright )
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.
These binaries have been distributed with the uclid_pa distribution.
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
The UCLID_PA configuration script will need the location of some of
these packages.
Papers and Documentation (relevant to the predicate
abstraction tool)
The UCLID user manual can be obtained from here (ps, pdf) and describes
the modeling language with some simple examples. The main changes
in the UCLID_PA models are described here.
In addition, please look at the set of examples
distributed with this version to write UCLID models.
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), LNCS 2725,
Springer-Verlag, Pages 141-153, Colorado, USA,
July 2003
"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.
"Indexed
Predicate Discovery for Unbounded System Verification"
Shuvendu K. Lahiri, Randal E. Bryant
In Proc. of Computer-Aided Verification
(CAV 04), Boston, July 2004 (to appear)
The most updated version of the above papers can be found in the following
Ph.D. thesis:
"Unbounded
System Verification Using Decision Procedure and Predicate Abstraction"
Shuvendu K. Lahiri.
Ph.D. Thesis, Carnegie Mellon
University, 2004.
Authors and Developers
This version of UCLID_PA has been developed by Shuvendu Lahiri. It builds
on the UCLID tool that was implemented by Shuvendu Lahiri and Sanjit Seshia
Email Shuvendu Lahiri
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