IBM Logo
IBM Research Lab in Haifa
Hot Shots  
FV Research in HRL  


E. Allen Emerson

University of Texas at Austin


Model Checking Systems with Many Subcomponents

Model checking is an algorithmic method for verifying correctness of finite state systems that originated as part of the speaker's dissertation work. Now, twenty years later, it is widely used in the computer hardware industry to formally verify and debug microprocessor designs, and is showing promise for software verification.

The chief limitation to the more widespread application of model checking is the state explosion problem, where the size of the system's global state graph grows exponentially with the number of subprocesses running concurrently in the system. This talk will examine various strategies for ameliorating state explosion. Some of these depend on exploiting the symmetry inherent in systems composed of many (nearly) homogeneous processes. Exponential savings are often possible. Others permit model checking an infinite family of uniformly parameterized systems (e.g., token rings of size n, for all n) in one fell swoop.