Invited Talk

Data-Abstraction Refinement: A Game Semantic Approach

Ranko Lazic

University of Warwick


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. Last updated: May 23, 2005