The Library
A contextual equivalence checker for IMJ*
Tools
Tools
Tools
Murawski, Andrzej S., Ramsay, Steven J. and Tzevelekos, Nikos (2015) A contextual equivalence checker for IMJ*. In: 13th International Symposium, ATVA 2015, Shanghai, China, 12-15 Oct 2015. Published in: Automated Technology for Verification and Analysis : Automated Technology for Verification and Analysis, 9364 pp. 234-240. ISBN 9783319249520. doi:10.1007/978-3-319-24953-7_19 ISSN 0302-9743.
|
PDF
WRAP_1271755-cs-010416-paper_96.pdf - Accepted Version - Requires a PDF viewer. Download (600Kb) | Preview |
Official URL: http://dx.doi.org/10.1007/978-3-319-24953-7_19
Abstract
We present coneqct: a contextual equivalence checking tool for terms of IMJ*, a fragment of Interface Middleweight Java for which the problem is decidable. Given two, possibly open (containing free identifiers), terms of the language, the contextual equivalence problem asks if the terms can be distinguished by any possible IMJ context. Although there has been a lot of prior work describing methods for constructing proofs of equivalence by hand, ours is the first tool to decide equivalences for a non-trivial, object-oriented language, completely automatically. This is achieved by reducing the equivalence problem to the emptiness problem for fresh-register pushdown automata. An evaluation demonstrates that our tool works well on examples taken from the literature.
| Item Type: | Conference Item (Paper) | ||||||
|---|---|---|---|---|---|---|---|
| Subjects: | Q Science > QA Mathematics > QA76 Electronic computers. Computer science. Computer software | ||||||
| Divisions: | Faculty of Science, Engineering and Medicine > Science > Computer Science | ||||||
| Library of Congress Subject Headings (LCSH): | Programming languages (Electronic computers) | ||||||
| Series Name: | Lecture Notes in Computer Science | ||||||
| Journal or Publication Title: | Automated Technology for Verification and Analysis : Automated Technology for Verification and Analysis | ||||||
| Publisher: | Springer | ||||||
| ISBN: | 9783319249520 | ||||||
| ISSN: | 0302-9743 | ||||||
| Book Title: | Automated Technology for Verification and Analysis | ||||||
| Editor: | Finkbeiner , Bernd and Pu , Geguang and Zhang, Lijun | ||||||
| Official Date: | 22 November 2015 | ||||||
| Dates: |
|
||||||
| Volume: | 9364 | ||||||
| Page Range: | pp. 234-240 | ||||||
| DOI: | 10.1007/978-3-319-24953-7_19 | ||||||
| Status: | Peer Reviewed | ||||||
| Publication Status: | Published | ||||||
| Access rights to Published version: | Restricted or Subscription Access | ||||||
| Date of first compliant deposit: | 8 April 2016 | ||||||
| Date of first compliant Open Access: | 8 April 2016 | ||||||
| Funder: | Engineering and Physical Sciences Research Council (EPSRC), Royal Academy of Engineering (Great Britain) | ||||||
| Grant number: | EP/J019577/1 (EPSRC) | ||||||
| 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
