UCLID

UCLID is a tool for verifying models of computer systems. It started out primarily focused on infinite-state systems (i.e., systems that, in addition to Boolean state variables, have state variables that are integer-valued or functions from integers to integers or Booleans), but now is equipped with techniques to also reason about word-level descriptions of systems (those with finite-precision types). The key component of UCLID is a decision procedure for a decidable fragment of first-order logic, including uninterpreted functions and equality, integer linear arithmetic, and constrained lambda expressions (for modeling arrays, memories, etc.). The decision procedure operates by translating the input formula to an equi-satisfiable Boolean formula on which it invokes a Boolean satisfiability (SAT) solver.

Applications of UCLID include microprocessor verification, protocol analysis, and analyzing software for security vulnerabilities. The decision procedure can also be used as a stand-alone theorem prover, or within other first-order or higher-order logic theorem provers.

Additional information and software is available from the UCLID webpage.

Here's a classification of my UCLID-related research: (somewhat out-of-date)

See below for detailed descriptions and links to papers.
 

UCLID Overview

The introductory UCLID paper was published in CAV'02. This describes the Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions (CLU), and shows how it can be used to model common features of infinite-state systems such as memories (arrays), queues, arrays of processes, etc. A decision procedure for CLU is also described, along with a listing of verification techniques available in UCLID. Experimental results demonstrate the scalability of our decision procedure.
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), LNCS 2404, Copenhagen, Denmark, July 2002.

A more recent paper describes the key features of UCLID's decision procedure and highlights differences with other procedures; one of these differences is that, unlike many other procedures, UCLID interprets variables over the integers rather than the rationals.

The UCLID Decision Procedure.
Shuvendu K. Lahiri and Sanjit A. Seshia.
Proc. of Intl. Conf. on Computer-Aided Verification (CAV), LNCS 3114, pages 475-478, July 2004.

 

Deciding Quantifier-free Presburger Arithmetic

Recently, UCLID's logic has been extended beyond CLU to include quantifier-free Presburger arithmetic, i.e., Boolean combinations of linear constraints over integer variables. There are currently two procedures, both of which operate by generating a SAT-encoding of the input formula.

The first method is an eager encoding technique that exploits features of formulas in software verification tasks. Specifically, many linear constraints tend to be separation (difference-bound) constraints and the non-separation constraints tend to be sparse. These features can be exploited in deriving a bound on the size of satisfying solutions to the formula, such that, if there is any solution, there is one within the bound. This bound can be used in generating a SAT-encoding, and results indicate that this procedure can greatly outperform others.

Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds.
Sanjit A. Seshia and Randal E. Bryant.
Proc. of 19th Annual IEEE Symposium on Logic in Computer Science (LICS), pages 100-109, July 2004.

An earlier, slightly more detailed version was published as a technical report. Its experimental results are somewhat out-of-date, though.
Deciding Quantifier-Free Presburger Formulas Using Finite Instantiation Based on Parameterized Solution Bounds.
Sanjit A. Seshia and Randal E. Bryant.
Computer Science Department Technical report CMU-CS-03-210, December 2003.

The second procedure performs a lazy encoding to SAT, starting with an approximate Boolean encoding that preserves completeness, and iteratively refining this encoding by using proofs of unsatisfiability generated by the SAT solver.

Abstraction-based Satisfiability Solving of Presburger Arithmetic.
Daniel Kroening, Joël Ouaknine, Sanjit A. Seshia, and Ofer Strichman.
Proc. of Intl. Conf. on Computer-Aided Verification (CAV), LNCS 3114, pages 308-320, July 2004.

 

Deciding CLU/Difference Logic

Originally, UCLID supported only a restricted subset of arithmetic variously called counter arithmetic, separation logic, or difference logic. Formulas in this logic are Boolean combinations of two-variable constraints called separation or difference-bound constraints (e.g., x > y + 3). For formulas in this logic, there are two encoding techniques UCLID used in translating to SAT.

The first technique is called the small-domain encoding method (also finite instantiation), in which integer variables are encoded as "large enough" bit-vectors. This is described in the paper below. The paper also describes how uninterpreted functions and constrained lambda expressions are handled by the decision procedure.

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), LNCS 2404, Copenhagen, Denmark, July 2002.

The second technique is variously called the per-constraint, EIJ, or direct encoding method. This is based on encoding each separation constraint with a corresponding Boolean variable, and adding "transitivity constraints" to the resulting encoding to preserve satisfiability. This is described in the paper below.

Deciding Separation Formulas with SAT.
Ofer Strichman, Sanjit A. Seshia, and Randal E. Bryant.
In Proc. Computer-Aided Verification (CAV), LNCS 2404, Copenhagen, Denmark, July 2002.

A more detailed version of this paper, with proofs, is available as a technical report.
Reducing Separation Formulas to Propositional Logic.
O. Strichman, S. A. Seshia, and R. E. Bryant.
Computer Science Department Technical report CMU-CS-02-132, April 2002.

Each of the above encodings has its strengths and weaknesses. The paper below analyzed these and presents a hybrid encoding method that is formula-specific. The resulting procedure yields impressive experimental results.

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), ACM Press, pages 425-430, June 2003.

We have also investigated the use of pseudo-Boolean solvers in place of SAT solvers. Here is a paper describing this work:

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.

 

Software Security

We have recently applied UCLID to problems in software security.

The following paper describes an application of UCLID to finding API-level security exploits, specifically format-string exploits.

Automatic Discovery of API-Level Exploits.
Vinod Ganapathy, Sanjit A. Seshia, Somesh Jha, Thomas W. Reps, and Randal E. Bryant.
27th International Conference on Software Engineering (ICSE), 2005. To appear.

 
  We have also used UCLID's decision procedure in the problem of detecting whether a program demonstrates known malicious behavior (such as a virus or worm). Here is a paper describing our first steps in this work.
Semantics-Aware Malware Detection.
Mihai Christodorescu, Somesh Jha, Sanjit A. Seshia, Dawn Song, and Randal E. Bryant.
IEEE Symposium on Security and Privacy, Oakland, May 2005. To appear.

 
 
 

Term-Level Bounded Model Checking

UCLID can be used for bounded model checking of an infinite-state system expressible in its logic. In general, model checking of such systems is not guaranteed to terminate, but it converges for many practical examples. The paper below gives a new convergence criterion along with semi-decision procedures to check this criterion.
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), LNCS 2860, pages 348-362, October 2003.

Proofs for theorems in this paper are available in the following technical report.
Convergence Testing in Term-Level Bounded Model Checking
R. E. Bryant, S. K. Lahiri, and S. A. Seshia.
Computer Science Department Technical report CMU-CS-03-156, June 2003.

 

Microprocessor Verification

UCLID has been used in verifying high-level microprocessor designs. Here is a paper describing one such case study.
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.