UCLID

What is UCLID?

UCLID (pronounced "Euclid") is a tool for modeling and verifying computational systems. Systems are modeled as transition systems where state and dynamics is represented in a subset of first-order logic with background theories. Verification methods employ efficient decision procedures based on a translation to Boolean satisfiability (SAT), also known as satisfiability modulo theories (SMT) solvers. The background theories currently supported by UCLID include uninterpreted functions and equality, finite-precision bit-vector arithmetic, arrays and restricted lambda expressions (useful for modeling data structures), and integer linear arithmetic. Both finite- and infinite-state systems can be modeled and verified with UCLID.

The UCLID verifier is one of the systems that helped pioneer the area of satisfiability modulo theories (SMT) and SMT-based formal verification.

Try out UCLID

Overview

The key component of UCLID are its "term-level" modeling language, and a collection of decision procedures for a decidable fragment of first-order logic, including uninterpreted functions and equality, integer linear arithmetic, finite-precision bit-vector arithmetic, and constrained lambda expressions (for modeling arrays, memories, etc.). The decision procedures operate by translating the input formula to an equi-satisfiable Boolean formula on which it invokes a Boolean satisfiability (SAT) solver.

Applications

Applications of UCLID include microprocessor verification, verifying network-on-chip designs, protocol analysis, verifying security-critical software, and verifying models of hybrid systems. The decision procedure can also be used as a stand-alone theorem prover, or within other first-order or higher-order logic theorem provers.

Acknowledgment

The UCLID project is funded through generous support from the Semiconductor Research Corporation (SRC contracts 1355.001, 2045.001, and 2460.001), Intel through the ISTC for Secure Computing, the Air Force Office of Scientific Research under MURI award FA9550-09-1-0539, the National Science Foundation (NSF grants CNS-0627734, CCF-0613997, and CNS-0644436), Microsoft Research, and Intel Corporation.