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.

References in zbMATH (referenced in 25 articles )

Showing results 1 to 20 of 25.
Sorted by year (citations)

1 2 next

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

1 2 next

Further publications can be found at: http://www.cs.cmu.edu/~uclid/#Papers