Hobbit: A Tool for Contextual Equivalence Checking Using Bisimulation Up-to Techniques

on YouTube ↗20m

" summary

Hobbit is a bounded model checker that verifies contextual equivalence for higher-order programs with local state by combining symbolic environmental bisimulations with up-to separation, up-to function re-entry and up-to invariance reductions. It emits SAT/CNF queries, is sound and complete up to the exploration bound, and cuts infinite games to finite representatives. On 173 examples it rises from 3 to 72 proven equivalences (most under 6s) and finds all 68 inequivalences (≈20s), with one case dropping >1000s to 5s.

AI-written summary · about

" chapters (14)

1. 0:00Intro
2. 0:35Contextual Equivalence of Higher-Order Programs
3. 1:44Symbolic Environmental Bisimulation
4. 2:52Simple Examples
5. 3:32Bounded Model Checking
6. 4:21Proving Equivalence
7. 6:00Finitising the Exploration
8. 8:01Up to Separation
9. 9:54Up to Function Re-entry
10. 11:03Up to State Invariants
11. 13:45Demo: Equivalence
12. 15:13Demo: Inequivalence
13. 16:29Performance of Up-to Techniques
14. 17:56Related Work