Abstract: UCLID is a verification tool for certain kinds of infinite-state systems, such as superscalar processors, parametrized process networks and communication protocols, that have state variables of unbounded integer type and unbounded arrays.

This talk will be divided into two parts.

I will first describe the CLU logic which underlies UCLID. CLU is a quantifier-free fragment of first-order logic with uninterpreted functions, equality, ordering, and increment and decrement operations. CLU can be used to model many interesting structures. I will describe an efficient decision procedure for CLU that leverages off recent advances in SAT solving, along with empirical results demonstrating its efficiency. (This part of the talk describes work that will appear in CAV'02.)

In the second half, I will describe ongoing work with UCLID, including applications and enhancements.

This work is joint with Randy Bryant and Shuvendu Lahiri.