Communications - November 2009

The converse of the theorem is not true as Figure 5 illustrates. A universal property that holds in the concrete system may fail to hold in the abstract system. For example, the property agF STOP (infinitely often STOP) holds in M, but not in Ma. Thus, a counterexample to the property in the abstract system may fail to be a counterexample in the concrete system. Such counterexamples are said to be spurious counterexamples. This leads to a verification technique called Counterexample Guided Abstraction Refinement (CEGAR). 12 Universal properties are checked on a series of increasingly precise abstractions of the original system. If the property holds, then by the Property Preservation Theorem, it must hold on the concrete system and we can stop. If it does not hold and we get a counterexample, then we must check the counterexample on the concrete system in order to make sure that it is not spurious. If the counterexample checks on the concrete system, then we have found an error and can also stop. If the counterexample is

spurious, then we use information in the counterexample to refine the abstraction mapping and repeat the loop. The CEGAR Loop in Figure 6 generalizes an earlier abstraction technique for sequential circuits called the localization reduction, which was developed by R. Kurshan. 32 CEGAR is used in many software model checkers including the SLAM Project at Microsoft. 1

2. 4. State Explosion Challenges for the Future

The state explosion problem is likely to remain the major challenge in model checking. There are many directions for future research on this problem, some of which are listed below.

• Software model checking, in particular, combining model checking and static analysis

• Effective model checking algorithms for real-time and hybrid systems

• Compositional model checking of complex systems

• Symmetry reduction and parameterized model checking

• Probabilistic and statistical model checking

• Combining model checking and theorem proving

• Interpreting long counterexamples

• Scaling up even more

3. JosePh sifaKis
the Quest foR coRRectness:
chaLLenGes anD PeRsPectiVes
3. 1. Where are We today?

Verification techniques have definitely found important applications. After the first two decades of intensive research and development, recent years have been characterized by a shift in focus and intensity.