×

UCLID

swMATH ID: 4657
Software Authors: Randal E. Bryant; Shuvendu K. Lahiri; Sanjit A. Seshia
Description: UCLID (pronounced ”Euclid”) is a tool for analyzing the correctness of models of hardware and software systems. UCLID can be used to model and verify infinite-state systems with variables of integer, Boolean, function, and array types. There are two main ways to use UCLID: As a verifier, for term-level bounded model checking, correspondence checking, deductive verification, and predicate abstraction-based verification. As a stand-alone decision procedure for the theories of uninterpreted functions and equality, integer linear arithmetic, and arrays. UCLID can also handle limited forms of quantification. The applications of UCLID explored to-date include microprocessor design verification, analyzing software for security exploits, and verifying distributed algorithms.
Homepage: http://www.cs.cmu.edu/~uclid/
Related Software: Chaff; PVS; MiniSat; SMT-LIB; cvc3; Siege; z3; Yices; MathSAT5; STP; CVC Lite; NQTHM; MONA; SIMPLIFY; BarcelogicTools; ESC/Java; VAMPIRE; CVC; zChaff; Lynx
Cited in: 24 Publications
Further Publications: http://www.cs.cmu.edu/~uclid/#Papers

Citations by Year