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*)

- UCLID overview
- Deciding quantifier-free Presburger arithmetic
- Deciding CLU/difference logic/separation logic
- Software security
- Term-level bounded model checking
- Microprocessor verification

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

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:

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.

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