Game−based software model checking: case studies and methodological considerations

Abstract

We introduce a new software modeling and model-checking tool, based on game semantics. The distinctive feature of the tool is its ability to model and verify program fragments, i.e. programs with undefined, non-local, identifiers. Through case studies, we show how this ability is useful in modeling certain classes of programs, such as protocols or modules. This feature is shown to be essential in the verification of abstract data-type invariants and equational properties. We explain how the observationally fully abstract models generated by the tool can economically represent very large internal state spaces.