From Bounded Checking to Verification of Equivalence via Symbolic up-to Techniques (Extended Abstract)

EasyChair Preprint 8780

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.

Keyphrases: Bounded Model Checking, contextual equivalence, operational game semantics, symbolic bisimulation, up-to techniques

@booklet{EasyChair:8780,
  author    = {Vasileios Koutavas and Yu-Yang Lin and Nikos Tzevelekos},
  title     = {From Bounded Checking to Verification of Equivalence via Symbolic up-to Techniques (Extended Abstract)},
  howpublished = {EasyChair Preprint 8780},
  year      = {EasyChair, 2022}}