dc.contributor.author | Koutavas, Vasileios | |
dc.contributor.author | Lin, Yu-Yang | |
dc.date.accessioned | 2022-03-21T09:49:50Z | |
dc.date.available | 2022-03-21T09:49:50Z | |
dc.date.created | 26 August 2021 | en |
dc.date.issued | 2021 | |
dc.date.submitted | 2021 | en |
dc.identifier.citation | Vasileios Koutavas, Yu-Yang Lin, Nikos Tzevelekos, Hobbit: A Tool for Contextual Equivalence Checking Using Bisimulation Up-to Techniques, ML Family Workshop 2021, online (collocated with ICFP 2021), 26 August 2021 | en |
dc.identifier.other | Y | |
dc.description.abstract | We present a bounded equivalence verification tool called Hobbit for higher-order programs with local state—based on a subset of OCaml—that combines fully abstract symbolic environmental bisimulations, novel up-to techniques, and lightweight invariant annotations. The tool reports no false positives or negatives, can automatically detect all inequivalences, and is able to automatically or semi-automatically prove many equivalences, including all classical Meyer and Sieber equivalences. | en |
dc.language.iso | en | en |
dc.rights | Y | en |
dc.subject | Operational game semantics | en |
dc.subject | Contextual equivalence | en |
dc.subject | Bounded model checking | en |
dc.subject | Symbolic bisimulation | en |
dc.subject | Up-to techniques | en |
dc.title | Hobbit: A Tool for Contextual Equivalence Checking Using Bisimulation Up-to Techniques | en |
dc.title.alternative | ML Family Workshop 2021 | en |
dc.type | Conference Paper | en |
dc.type.supercollection | scholarly_publications | en |
dc.type.supercollection | refereed_publications | en |
dc.identifier.peoplefinderurl | http://people.tcd.ie/vkoutav | |
dc.identifier.rssinternalid | 239709 | |
dc.rights.ecaccessrights | openAccess | |
dc.subject.TCDTag | BISIMULATION | en |
dc.subject.TCDTag | computer science theory | en |
dc.subject.TCDTag | contextual equivalence | en |
dc.subject.TCDTag | model checking | en |
dc.subject.TCDTag | operational game semantics | en |
dc.subject.TCDTag | software verification | en |
dc.identifier.rssuri | https://icfp21.sigplan.org/details/mlfamilyworkshop-2021-papers/1/Hobbit-A-Tool-for-Contextual-Equivalence-Checking-Using-Bisimulation-Up-to-Technique | |
dc.identifier.orcid_id | 0000-0002-3970-2486 | |
dc.status.accessible | N | en |
dc.contributor.sponsor | Science Foundation Ireland (SFI) | en |
dc.contributor.sponsorGrantNumber | 13/RC/2094 | en |
dc.identifier.uri | http://hdl.handle.net/2262/98313 | |