Model checking is an algorithmic method for formally verifying the correctness of finite state concurrent systems. It is an ideal verification technique for many cost- and safety-critical systems. It has gained widespread acceptance in the computer hardware industry, and it is showing promise for software verification as well.

The major challenge in applying model checking to large systems is the state explosion problem -- the size of the state transition graph grows exponentially with the number of concurrent subcomponents. Due to state explosion, most industrial-scale designs cannot be handled directly by model checkers. Abstraction is a key in addressing this major challenge. This talk will present several new automatic abstraction refinement techniques, which have significantly increased the ability of model checkers to handle large real-world designs.

Biographical sketch:

Chao Wang is a Ph.D. candidate in the University of Colorado at Boulder. His research is in the area of formal methods for specification and verification of concurrent systems. He received his B.S. in Electrical Engineering in 1996 from Peking University, China. From 1996 to 1999, he was a research assistant in Peking University. From 1999 to 2000, he worked in industry as a hardware engineer.