UCLID
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.
Keywords for this software
References in zbMATH (referenced in 25 articles )
Showing results 1 to 20 of 25.
Sorted by year (- Davenport, James H.; England, Matthew; Griggio, Alberto; Sturm, Thomas; Tinelli, Cesare: Symbolic computation and satisfiability checking (2020)
- Bozzano, Marco; Cimatti, Alessandro; Mattarei, Cristian: Formal reliability analysis of redundancy architectures (2019)
- Cheng, Xi; Zhou, Min; Song, Xiaoyu; Gu, Ming; Sun, Jiaguang: Parallelizing SMT solving: lazy decomposition and conciliation (2018)
- Kuncak, Viktor; Piskac, Ruzica; Suter, Philippe; Wies, Thomas: Building a calculus of data structures (2010)
- Brummayer, Robert; Biere, Armin: Lemmas on demand for the extensional theory of arrays (2009)
- Wies, Thomas; Piskac, Ruzica; Kuncak, Viktor: Combining theories with shared set operations (2009)
- Piskac, Ruzica; Kuncak, Viktor: Linear arithmetic with stars (2008)
- Bryant, Randal E.; Kroening, Daniel; Ouaknine, Joël; Seshia, Sanjit A.; Strichman, Ofer; Brady, Bryan: Deciding bit-vector arithmetic with abstraction (2007)
- Christodorescu, Mihai; Jha, Somesh; Kinder, Johannes; Katzenbeisser, Stefan; Veith, Helmut: Software transformations to improve malware detection. (2007) ioport
- Ganesh, Vijay; Dill, David L.: A decision procedure for bit-vectors and arrays (2007)
- Kim, Hyondeuk; Jin, Hoonsang; Somenzi, Fabio: Disequality management in integer difference logic via finite instantiations. (2007)
- Kuncak, Viktor; Rinard, Martin: Towards efficient satisfiability checking for Boolean algebra with Presburger arithmetic (2007)
- Sebastiani, Roberto: Lazy satisfiability modulo theories (2007)
- Bryant, Randal E.: Formal verification of infinite state systems using Boolean methods (2006)
- Kuncak, Viktor; Nguyen, Huu Hai; Rinard, Martin: Deciding Boolean algebra with Presburger arithmetic (2006)
- Lahiri, Shuvendu K.; Mehra, Krishna K.: Interpolant based decision procedure for quantifier-free Presburger arithmetic (2006)
- Manolios, Panagiotis; Srinivasan, Sudarshan K.: A framework for verifying bit-level pipelined machines based on automated deduction and decision procedures (2006)
- Rodeh, Yoav; Strichman, Ofer: Building small equality graphs for deciding equality logic with uninterpreted functions (2006)
- Ball, Thomas; Lahiri, Shuvendu K.; Musuvathi, Madanlal: Zap: Automated theorem proving for software analysis (2005)
- Bryant, Randal E.; Seshia, Sanjit A.: Decision procedures customized for formal verification (2005)
Further publications can be found at: http://www.cs.cmu.edu/~uclid/#Papers