Formal verification tools have advanced to the point where they are routinely used to verify real-life hardware systems and protocols. Engineers designing complex subsystems, such as coherent caches and floating-point units, use formal verification to track down bugs that
may only occur rarely, but with disastrous consequences when they do. To date, most successful formal verification tools are based on a bit-level model of computation. Using powerful inference engines, such as Binary Decision Diagrams (BDDs) and Boolean satisfiability (SAT) checkers, symbolic model checkers and similar tools can analyze all possible behaviors of very large, finite-state systems. For many hardware and software systems, we would like to go beyond bit-level models to handle systems that are truly infinite state, or that are better modeled as infinite-state systems. Examples include: systems containing buffers of arbitrary size, programs manipulating integer data, and concurrency protocols involving an arbitrary number of  processes.

Historically, much of the effort in verifying such systems has involved automated theorem provers, requiring considerable guidance and expertise on the part of the user. Instead, we would like to devise approaches for these more powerful computational models that retain the desirable features of model checking, such as the high degree of automation and the ability to generate counterexamples. We have developed UCLID, a prototype verifier for infinite-state systems. The UCLID modeling language extends that of SMV, a bit-level model checker, to include integer and function state variables, addition by constants, and relational operations. The underlying logic is expressive enough to model a wide range of systems, but it still permits a decision procedure where we transform the formula into propositional logic and then use either BDDs or a SAT solver. Most recently, we have developed powerful  predicate abstraction methods that can automatically generate and prove system invariants using techniques similar those used in symbolic model checking.