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

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. ISSN 0302-9743. doi:10.1007/978-3-319-24953-7_19

[img]
Preview
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

Request Changes to record.

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 > 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:
DateEvent
22 November 2015Published
18 June 2015Accepted
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
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 View Item

Downloads

Downloads per month over past year

View more statistics

twitter

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