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. ps, pdf.

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.

**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. ps, pdf.

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.

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 Bit-Vector Arithmetic with Abstraction.**Randal E. Bryant, Daniel Kroening, Joel Ouaknine, Sanjit A. Seshia, Ofer Strichman, and Bryan Brady. In 13th Intl. Conference on Tools and Algorithms for the Construction of Systems (TACAS), March 2007 (to appear). pdf

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.

**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. ps, pdf

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. html

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. ps, pdf

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. ps, pdf

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. ps, pdf

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. html

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. ps, pdf

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. ps, pdf

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

**Verification with Small and Short Worlds.**Rohit Sinha, Cynthia Sturton, Petros Maniatis, Sanjit A. Seshia, and David Wagner. In Proceedings of the IEEE International Conference on Formal Methods in Computer-Aided Design (FMCAD), 2012. pdf**Formal Modeling and Verification of CloudProxy.**Wei Yang Tan, Rohit Sinha, John Manferdelli, and Sanjit A. Seshia. In Proceedings of the Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE), 2014. pdf

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.

**Symbolic Software Model Validation.**Cynthia Sturton, Rohit Sinha, Thurston H.Y. Dang, Sakshi Jain, Michael McCoyd, Wei-Yang Tan, Petros Maniatis, Sanjit A. Seshia, and David Wagner. In Proceedings of the 10th ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE), October 2013. pdf

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.

**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. ps, pdf

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. pdf

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. ps, pdf

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. html

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

**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. ps, pdf

**Term-Level Verification of a Pipelined CISC Microprocessor.**Randal E. Bryant. Computer Science Department Technical Report CMU-CS-05-195, December 2005. html