We present a semantic framework for data abstraction and refinement for verifying safety properties of open programs. The presentation is focused on an Algol-like programming language that incorporates data abstraction in its syntax. The fully abstract game semantics of the language is used for model-checking safety properties, and an interaction-sequence-based semantics is used for interpreting potentially spurious counterexamples and computing refined abstractions for the next iteration. We show that the abstraction refinement procedure is a semi-algorithm.
Joint work with Aleksandar Dimovski and Dan Ghica.
| rupak@cs.ucla.edu | Last updated: May 23, 2005 |