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.


References in zbMATH (referenced in 21 articles )

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

1 2 next

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

1 2 next


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