home · mobile · calendar · bactac · 2003-2004 · 


Abstraction Refinement for Large Scale Model Checking
Grad Student, Department of Electrical and Computer Engineering

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.

Department of Computer Science
University of Colorado Boulder
Boulder, CO 80309-0430 USA
May 5, 2012 (14:24)