Hobbit: A Tool for Contextual Equivalence Checking Using Bisimulation Up-to Techniques
File Type:
PDFItem Type:
Conference PaperDate:
2021Access:
openAccessCitation:
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 2021Download Item:
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.
Sponsor
Grant Number
Science Foundation Ireland (SFI)
13/RC/2094
Author's Homepage:
http://people.tcd.ie/vkoutav
Author: Koutavas, Vasileios; Lin, Yu-Yang
Sponsor:
Science Foundation Ireland (SFI)Other Titles:
ML Family Workshop 2021Type of material:
Conference PaperCollections
Availability:
Full text availableKeywords:
Operational game semantics, Contextual equivalence, Bounded model checking, Symbolic bisimulation, Up-to techniquesSubject (TCD):
BISIMULATION , computer science theory , contextual equivalence , model checking , operational game semantics , software verificationMetadata
Show full item recordLicences: