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.