Falsifying Safety Properties Through Games on Over-approximating Models

Abstractions of programs are traditionally over-approximations and have proved to be useful for the verification of safety properties. They are presently perceived as being useless for the falsification of safety properties, i.e. showing that program execution definitely reaches a “bad” state. Alternative techniques, such as the computation of under-approximating must transitions, have addressed this shortcoming in the past. We show that over-approximating models can indeed falsify safety properties by relying on and exploiting the seriality and partial determinism of programs: programs don't just stop for no reason, and most program statements have deterministic semantics. Our method is based on solving a two-person attractor game derived from over-approximating models and makes no assumptions about the abstraction domain used. An example demonstrates the successful use of our approach, and highlights the role played by seriality and our handling of nondeterminism. Finally, we show that our method can encode must transitions, if supplied, by a simple modification of the ownership of nodes in the attractor game derived from the over-approximating model.