Formal Verification of Infinite State Systems using Boolean Methods
Speaker: Professor Randal E. Bryant , Carnegie Mellon University
Date: February 9 2006
Time: 4:00PM to 5:30PM
Location: 32-123
Host: Victor Zue, CSAIL
Contact: Victoria Palay, 617-253-8924, palay@csail.mit.edu
Relevant URL: 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.
BIOGRAPHY
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.
See other events that are part of Dertouzos Lecturer Series 2005/2006
See other events happening in February 2006
