Journal Title
Title of Journal: Int J Softw Tools Technol Transfer
|
Abbravation: International Journal on Software Tools for Technology Transfer
|
Publisher
Springer-Verlag
|
|
|
|
|
|
Authors: Adam Bakewell Aleksandar Dimovski Dan R Ghica Ranko Lazić
Publish Date: 2010/03/14
Volume: 12, Issue: 5, Pages: 373-389
Abstract
This paper presents a semantic framework for data abstraction and refinement for verifying safety properties of open programs with integer types The presentation is focused on an Algollike programming language that incorporates data abstraction in its type system We use a fully abstract game semantics in the style of Hyland and Ong and a more intensional version of the model that tracks nondeterminism introduced by abstraction in order to detect false counterexamples These theoretical developments are incorporated in a new modelchecking tool Mage which implements efficiently the dataabstraction refinement procedure using symbolic and onthefly techniques
Keywords:
.
|
Other Papers In This Journal:
|