Professor Randal E. Bryant from the Carnegie Mellon University gave a talk titled
"Formal Verification of Infinite State Systems using Boolean Methods" on February 9th, 2006.
Abstract:
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 arbitrary numbers of processes.
Historically, much of the effort in verifying such systems 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. 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.
Bio:
Randal E. Bryant is Dean of the Carnegie Mellon University School of Computer Science. He has been on the faculty at Carnegie Mellon for 21 years, starting as an Assistant Professor and progressing to his current rank of University Professor.
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 has received widespread recognition for his work. He 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. He received his S.M. (1977) and Ph.D. (1981) degress from MIT and was a member of the Laboratory for Computer Science, doing research on distributed simulation and transistor-level logic simulation. He was on the faculty at Caltech from 1981 to 1984.
For more information:
Dr. Randal E. Bryant's home page
CSAIL Dertouzos Lecturer Series Archive