Model-checking contextual equivalence of higher-order programs with references

This talk will present SyTeCi, a general automated tool to check
contextual equivalence for programs written in a typed higher-order
language with references (i.e. local mutable states), corresponding to
a fragment of OCaml. After introducing the notion of contextual
equivalence, we will see on some examples why it is hard to prove such
equivalences (reentrant calls, private states). Then, we will
introduce SyTeCi, a tool to automatically check such equivalences.
This tool is based on a reduction of the problem of contextual
equivalence of two programs to the problem of reachability of “error
states” in a transition system of memory configurations. Contextual
equivalence being undecidable (even in a finitary setting), so does
the non-reachability problem for such transition systems. However, one
can apply model-checking techniques (predicate abstraction, analysis
of pushdown systems) to check non-reachability via some
approximations. This allows us to prove automatically many non-trivial
examples of the literature, that could only be proved by hand before.
We will end this talk by the presentation of a prototype implementing
this work.