UCLID

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.

A somewhat 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.

Recently, UCLID's logic has been extended beyond CLU to include finite-precision bit-vector arithmetic and quantifier-free Presburger arithmetic. The decision procedures for these logics are described below.


Deciding Finite-Precision Bit-Vector Arithmetic

UCLID's decision procedure for finite-precision bit-vector arithmetic operates by translating the original bit-vector formula F to SAT based on iterative construction of under- and over-approximations to F. Here is a paper describing the algorithm and experimental results.


Deciding Quantifier-free Presburger Arithmetic

Quantifier-free Presburger arithmetic formulas are 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.

An earlier, slightly more detailed version was published as a technical report. Its experimental results are somewhat out-of-date, though.

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.


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.

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.

A more detailed version of this paper, with proofs, is available as a technical report.

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.

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


Software Security

Recently, we applied UCLID for proving properties of low-level, security-critical software like hypervisors and CPU emulators.

In the following paper, we present a technique for proving that a UCLID model simulates a C/C++ program. We apply this tool to UCLID models of C programs such as component of Bochs emulator, XMHF hypervisor, and ftpd.

In past, we have 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.

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.


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.

Proofs for theorems in this paper are available in the following technical report.


Microprocessor Verification

UCLID has been used in verifying high-level microprocessor designs. Below are two case studies.