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:

  1. 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.
  2. 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.

  1. Version 0.1 uses Daniel Kroening's SATQE binary for performing quantifier elimination from an existentially quantified Boolean formula. 
  2. 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:

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