The Library
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
|
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
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: |
|
||||||
| Date of first compliant deposit: | 8 April 2016 | ||||||
| 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 |
Downloads
Downloads per month over past year
