dc.contributor.author | Koutavas, Vasileios | en |
dc.date.accessioned | 2022-03-21T09:31:23Z | |
dc.date.available | 2022-03-21T09:31:23Z | |
dc.date.created | 2-7 April 2022 | en |
dc.date.issued | 2022 | en |
dc.date.submitted | 2022 | en |
dc.identifier.citation | Vasileios Koutavas, Yu-Yang Lin, Nikos Tzevelekos, From Bounded Checking to Verification of Equivalence via Symbolic Up-to Techniques, LNCS, 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (ETAPS 2020), Munich, Germany, 2-7 April 2022, 13244, Springer, 2022, 178 - 195 | en |
dc.identifier.other | Y | en |
dc.identifier.uri | http://hdl.handle.net/2262/98311 | |
dc.description | PUBLISHED | en |
dc.description | Munich, Germany | en |
dc.description.abstract | We present a bounded equivalence verification technique for higher-order programs with local state. This technique combines fully abstract symbolic environmental bisimulations similar to symbolic game semantics, novel up-to techniques, and lightweight state invariant annotations. This yields an equivalence verification technique with no false positives or negatives. The technique is bounded-complete, in that all inequivalences are automatically detected given large enough bounds.
Moreover, several hard equivalences are proved automatically or after being annotated with state invariants. We realise the technique in a tool prototype called Hobbit and benchmark it with an extensive set of new and existing examples. Hobbit can prove many classical equivalences including all Meyer and Sieber examples. | en |
dc.format.extent | 178 | en |
dc.format.extent | 195 | en |
dc.language.iso | en | en |
dc.publisher | Springer | en |
dc.relation.ispartofseries | 13244 | en |
dc.rights | Y | en |
dc.subject | Contextual equivalence | en |
dc.subject | Bounded model checking | en |
dc.subject | Symbolic bisimulation | en |
dc.subject | Up-to techniques | en |
dc.subject | Operational game semantics | en |
dc.title | From Bounded Checking to Verification of Equivalence via Symbolic Up-to Techniques | en |
dc.title.alternative | LNCS | en |
dc.title.alternative | 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (ETAPS 2020) | 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 | en |
dc.identifier.rssinternalid | 239697 | en |
dc.identifier.doi | https://doi.org/10.1007/978-3-030-99527-0_10 | en |
dc.rights.ecaccessrights | openAccess | |
dc.subject.TCDTag | BISIMULATION | en |
dc.subject.TCDTag | Formal Semantics | en |
dc.subject.TCDTag | contextual equivalence | en |
dc.subject.TCDTag | model checking | en |
dc.subject.TCDTag | operational game semantics | en |
dc.subject.TCDTag | programming language theory | en |
dc.subject.TCDTag | software verification | en |
dc.identifier.rssuri | https://link.springer.com/chapter/10.1007/978-3-030-99527-0_10 | en |
dc.identifier.orcid_id | 0000-0002-3970-2486 | en |
dc.status.accessible | N | en |
dc.contributor.sponsor | Science Foundation Ireland (SFI for RF) | en |
dc.contributor.sponsorGrantNumber | 13/RC/2094_2 | en |