Publications Home » Falsifying safety properties thro...
Falsifying safety properties through games on over-approximating models
Nathaniel Charlton, Michael Huth
- Conference or Workshop Paper
- Second Workshop on Reachability Problems
- 2008
- Electronic Notes in Theoretical Computer Science
- Elsevier
- Abstract
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.
PDF of full publication (701 kilobytes)- (need help viewing PDF files?)
BibTEX file for the publication - Copyright notice
The PDF contains a preliminary version of the final version of this paper.
- N.B.
- Conditions for downloading publications from this site.
pubs.doc.ic.ac.uk: built & maintained by Ashok Argent-Katwala.