Abstract: Formal verification tools have advanced to the point where they are routinely used to verify complex 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, and programs manipulating integer data. 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 quite expressive, but it still permits a decision procedure where we transform the formula into propositional logic and then use either BDDs or a SAT solver. We demonstrate UCLID's modeling and verification capabilities with such examples as out-of-order microprocessors, and directory-based cache coherency protocols.

Randal E. Bryant is Dean of the Carnegie Mellon University School of Computer Science. He has been on the faculty at Carnegie Mellon since 1984. Dr. Bryant's research focuses on methods for formally verifying digital hardware, and more recently some forms of software. His 1986 paper on symbolic Boolean manipulation using Ordered Binary Decision Diagrams (BDDs) has the highest citation count of any publication in the Citeseer database of computer science literature. In addition, he has developed several techniques to verify circuits by symbolic simulation, with levels of abstraction ranging from transistors to very high-level representations. Dr. Bryant is a fellow of the IEEE and the ACM, as well as a member of the National Academy of Engineering. His awards include the 1997 ACM Kanellakis Theory and Practice Award (shared with Edmund M. Clarke, Ken McMillan, and Allen Emerson) for contributing to the development of symbolic model checking, as well as the 1989 IEEE W.R.G. Baker Prize for the best paper appearing in any IEEE publication during the preceding year. Dr. Bryant received his B.S. in Applied Mathematics from the University of Michigan in 1973, and his PhD from MIT in 1981. He was on the faculty at Caltech from 1981 to 1984.