Electrical Engineering
      and Computer Sciences

Electrical Engineering and Computer Sciences

COLLEGE OF ENGINEERING

UC Berkeley

   

2010 Research Summary

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

View Current Project Information

Sanjit A. Seshia, Bryan Brady, Susmit Jha and Rhishikesh Shrikant Limaye

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.