UCLID: Reasoning about Computer Systems with Boolean Methods (UCLID)

Sanjit A. Seshia and Rohit Sinha

UCLID is a toolkit for verifying models of computer systems. Applications of UCLID include microprocessor verification, protocol analysis, analyzing software for security vulnerabilities, malware detection and analysis, and verifying models of hybrid systems. 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, finite-precision bit-vector arithmetic, and constrained lambda expressions (used, for example, to model arrays and memories). The decision procedure operates by translating the input formula to an equi-satisfiable Boolean formula on which it invokes a Boolean satisfiability (SAT) solver.