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

- 11:00 22nd May 2019 ( week 4, Trinity Term 2019 )051

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.