UCLID's Elements: Term-Level Verification and SMT Solving

UCLID is a toolkit for modeling and verifying systems, both finite- and infinite-state, at the term level. The phrase "term level" refers to the use of first-order logic with background theories in modeling and verification. This talk will describe the key elements of UCLID: (i) term-level abstraction -- the process of creating term-level models from implementations; (ii) term-level verification -- the verification strategies available in UCLID, and (iii) SMT solving -- the decision procedures within UCLID that form its computational engine. UCLID has been applied to several application areas, including hardware verification and synthesis, computer security, software analysis, and hybrid systems verification --- this talk will touch upon some of these applications.

Talk slides available here in PDF.

Randy Bryant & Sanjit Seshia, CMU, Pittsburgh and UC, Berkeley, USA

Click here for biographies: Randy Bryant, Sanjit Seshia