Bakewell, Adam, Dimovski, Aleksandar, Ghica, Dan R. and Lazic, Ranko. (2010) Data-abstraction refinement : a game semantic approach. International Journal on Software Tools for Technology Transfer, Vol.12 (No.5). pp. 373-389. ISSN 1433-2779

Full text not available from this repository.

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 Algol-like 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 model-checking tool, Mage, which implements efficiently the data-abstraction refinement procedure using symbolic and on-the-fly techniques.

Item Type:	Journal Article
Subjects:	Q Science > QA Mathematics > QA76 Electronic computers. Computer science. Computer software
Divisions:	Faculty of Science > Computer Science
Library of Congress Subject Headings (LCSH):	Game theory -- Computer programs, Game-theoretical semantics, Computer simulation, Programming languages (Electronic computers)
Journal or Publication Title:	International Journal on Software Tools for Technology Transfer
Publisher:	Springer
ISSN:	1433-2779
Date:	September 2010
Volume:	Vol.12
Number:	No.5
Page Range:	pp. 373-389
Identification Number:	10.1007/s10009-010-0143-0
Status:	Peer Reviewed
Publication Status:	Published
Access rights to Published version:	Restricted or Subscription Access
Funder:	Engineering and Physical Sciences Research Council (EPSRC)
Grant number:	GR/S52759/01 (EPSRC), EP/D034906/1 (EPSRC)
URI:	http://wrap.warwick.ac.uk/id/eprint/37075

Request changes to a record

Actions (login required)

View Item