Skip to content Skip to navigation
University of Warwick
  • Study
  • |
  • Research
  • |
  • Business
  • |
  • Alumni
  • |
  • News
  • |
  • About

University of Warwick
Publications service & WRAP

Highlight your research

  • WRAP
    • Home
    • Search WRAP
    • Browse by Warwick Author
    • Browse WRAP by Year
    • Browse WRAP by Subject
    • Browse WRAP by Department
    • Browse WRAP by Funder
    • Browse Theses by Department
  • Publications Service
    • Home
    • Search Publications Service
    • Browse by Warwick Author
    • Browse Publications service by Year
    • Browse Publications service by Subject
    • Browse Publications service by Department
    • Browse Publications service by Funder
  • Help & Advice
University of Warwick

The Library

  • Login
  • Admin

Game semantic analysis of equivalence in IMJ

Tools
- Tools
+ Tools

Murawski, Andrzej S., Ramsay, Steven J. and Tzevelekos, Nikos (2015) Game semantic analysis of equivalence in IMJ. In: 13th International Symposium, ATVA 2015,, Shanghai, China, 12-15 Oct 2015. Published in: Automated Technology for Verification and Analysis, 9364 pp. 411-428. ISSN 0302-9743. doi:10.1007/978-3-319-24953-7_30

[img]
Preview
PDF
WRAP_1271755-cs-010416-paper_61.pdf - Accepted Version - Requires a PDF viewer.

Download (794Kb) | Preview
Official URL: http://dx.doi.org/10.1007/978-3-319-24953-7_30

Request Changes to record.

Abstract

Using game semantics, we investigate the problem of verifying contextual equivalences in Interface Middleweight Java (IMJ), an imperative object calculus in which program phrases are typed using interfaces. Working in the setting where data types are non-recursive and restricted to finite domains, we identify the frontier between decidability and undecidability by reference to the structure of interfaces present in typing judgments. In particular, we show how to determine the decidability status of problem instances (over a fixed type signature) by examining the position of methods inside the term type and the types of its free identifiers. Our results build upon the recent fully abstract game semantics of IMJ. Decidability is proved by translation into visibly pushdown register automata over infinite alphabets with fresh-input recognition.

Item Type: Conference Item (Paper)
Subjects: Q Science > QA Mathematics > QA76 Electronic computers. Computer science. Computer software
Divisions: Faculty of Science > Computer Science
Library of Congress Subject Headings (LCSH): Programming languages (Electronic computers), Java (Computer program language)
Series Name: Lecture Notes in Computer Science
Journal or Publication Title: Automated Technology for Verification and Analysis
ISSN: 0302-9743
Book Title: Automated Technology for Verification and Analysis : 13th International Symposium, ATVA 2015, Shanghai, China, October 12-15, 2015, Proceedings
Editor: Finkbeiner , Bernd and Pu , Geguang and Zhang , Lijun
Official Date: 22 November 2015
Dates:
DateEvent
22 November 2015Published
18 June 2015UNSPECIFIED
Volume: 9364
Page Range: pp. 411-428
DOI: 10.1007/978-3-319-24953-7_30
Status: Peer Reviewed
Publication Status: Published
Description:
Conference Paper Type: Paper
Title of Event: 13th International Symposium, ATVA 2015,
Type of Event: Conference
Location of Event: Shanghai, China
Date(s) of Event: 12-15 Oct 2015

Request changes or add full text files to a record

Repository staff actions (login required)

View Item View Item

Downloads

Downloads per month over past year

View more statistics

twitter

Email us: wrap@warwick.ac.uk
Contact Details
About Us