×

zbMATH — the first resource for mathematics

Data-abstraction refinement: A game semantic approach. (English) Zbl 1141.68366
Hankin, Chris (ed.) et al., Static analysis. 12th international symposium, SAS 2005, London, UK, September 7–9, 2005. Proceedings. Berlin: Springer (ISBN 3-540-28584-9/pbk). Lecture Notes in Computer Science 3672, 102-117 (2005).
Summary: This paper presents 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.
For the entire collection see [Zbl 1087.68004].

MSC:
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
68Q55 Semantics in the theory of computing
Software:
SLAM; HOMER; BLAST
PDF BibTeX XML Cite
Full Text: DOI