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 all top 5 Cited by 42 Authors 5 Kuncak, Viktor 4 Bryant, Randal E. 4 Lahiri, Shuvendu Kumar 4 Seshia, Sanjit Arunkumar 3 Piskac, Ruzica 3 Strichman, Ofer 2 Manolios, Panagiotis 2 Rinard, Martin C. 2 Srinivasan, Sudarshan K. 2 Wies, Thomas 1 Ball, Thomas 1 Biere, Armin 1 Bozzano, Marco 1 Brady, Bryan A. 1 Brummayer, Robert 1 Cheng, Xi 1 Cimatti, Alessandro 1 Davenport, James Harold 1 Dill, David L. 1 England, Matthew 1 Ganesh, Vijay 1 Griggio, Alberto 1 Jin, HoonSang 1 Kim, Hyondeuk 1 Kröning, Daniel 1 Mattarei, Cristian 1 Mehra, Krishna K. 1 Meir, Orly 1 Musuvathi, Madanlal 1 Nguyen, Huu Hai 1 Nieuwenhuis, Robert 1 Oliveras, Albert 1 Ouaknine, Joel O. 1 Rodeh, Yoav 1 Sebastiani, Roberto 1 Somenzi, Fabio 1 Song, Xiaoyu 1 Sturm, Thomas 1 Sun, Jiaguang 1 Suter, Philippe 1 Tinelli, Cesare 1 Zhou, Min all top 5 Cited in 6 Serials 4 Journal of Satisfiability, Boolean Modeling and Computation 2 Journal of Automated Reasoning 1 Artificial Intelligence 1 Journal of Symbolic Computation 1 Information and Computation 1 Formal Aspects of Computing Cited in 5 Fields 24 Computer science (68-XX) 8 Mathematical logic and foundations (03-XX) 1 General and overarching topics; collections (00-XX) 1 Number theory (11-XX) 1 Field theory and polynomials (12-XX) Citations by Year