A counter-example guided abstraction refinement scheme for parameterized verification
- Date and Time
Thursday, October 14th, 2010 at 10:30
Polacksbacken, room 1145
I will introduce a recent work (CONCUR 2010). First, I will recall the approach of monotonic abstraction to verify systems with an arbitrary number of concurrent and communicating processes, i.e., parameterized systems. Monotonic abstraction is particularly successful in automatic verification of safety properties for parameterized systems. The main drawback is that it sometimes generates spurious counter-examples.
I will describe a counterexample-guided abstraction refinement (CEGAR) framework for monotonic abstraction. The CEGAR algorithm automatically extracts from each spurious counterexample a set of configurations called a "Safety Zone"and uses it to refine the abstract transition system of the next iteration. This approach gave encouraging results and allowed the verification of several parameterized systems.