Programming Research Group
Research Report RR-03-11
Game-based software model checking: case studies and methodological considerations
Dan R. Ghica
May 2003, 23pp.
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.
This paper is available as a 246772 bytes gzipped PostScript file.
|
![[Oxford Spires]](/im/spires.gif){kind=small}
oucl