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 22 articles )

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

1 2 next

  1. Cheng, Xi; Zhou, Min; Song, Xiaoyu; Gu, Ming; Sun, Jiaguang: Parallelizing SMT solving: lazy decomposition and conciliation (2018)
  2. Kuncak, Viktor; Piskac, Ruzica; Suter, Philippe; Wies, Thomas: Building a calculus of data structures (2010)
  3. Brummayer, Robert; Biere, Armin: Lemmas on demand for the extensional theory of arrays (2009)
  4. Wies, Thomas; Piskac, Ruzica; Kuncak, Viktor: Combining theories with shared set operations (2009)
  5. Piskac, Ruzica; Kuncak, Viktor: Linear arithmetic with stars (2008)
  6. Christodorescu, Mihai; Jha, Somesh; Kinder, Johannes; Katzenbeisser, Stefan; Veith, Helmut: Software transformations to improve malware detection. (2007) ioport
  7. Ganesh, Vijay; Dill, David L.: A decision procedure for bit-vectors and arrays (2007)
  8. Kim, Hyondeuk; Jin, Hoonsang; Somenzi, Fabio: Disequality management in integer difference logic via finite instantiations. (2007)
  9. Kuncak, Viktor; Rinard, Martin: Towards efficient satisfiability checking for Boolean algebra with Presburger arithmetic (2007)
  10. Sebastiani, Roberto: Lazy satisfiability modulo theories (2007)
  11. Bryant, Randal E.: Formal verification of infinite state systems using Boolean methods (2006)
  12. Kuncak, Viktor; Nguyen, Huu Hai; Rinard, Martin: Deciding Boolean algebra with Presburger arithmetic (2006)
  13. Lahiri, Shuvendu K.; Mehra, Krishna K.: Interpolant based decision procedure for quantifier-free Presburger arithmetic (2006)
  14. Manolios, Panagiotis; Srinivasan, Sudarshan K.: A framework for verifying bit-level pipelined machines based on automated deduction and decision procedures (2006)
  15. Rodeh, Yoav; Strichman, Ofer: Building small equality graphs for deciding equality logic with uninterpreted functions (2006)
  16. Ball, Thomas; Lahiri, Shuvendu K.; Musuvathi, Madanlal: Zap: Automated theorem proving for software analysis (2005)
  17. Bryant, Randal E.; Seshia, Sanjit A.: Decision procedures customized for formal verification (2005)
  18. Manolios, Panagiotis; Srinivasan, Sudarshan K.: A parameterized benchmark suite of hard pipelined-machine-Verification problems (2005)
  19. Meir, Orly; Strichman, Ofer: Yet another decision procedure for equality logic (2005)
  20. Nieuwenhuis, Robert; Oliveras, Albert: Decision procedures for SAT, SAT modulo theories and beyond. The BarcelogicTools (2005)

1 2 next

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