Abstract
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.
Original language | English |
---|---|
Pages (from-to) | 102-117 |
Number of pages | 16 |
Journal | Lecture Notes in Computer Science |
Volume | 3672 |
DOIs | |
Publication status | Published - 1 Jan 2005 |
Event | Static Analysis: 12th International Symposium (SAS 2005) - Duration: 1 Jan 2005 → … |