206
22 March 2018 - 16h00
Model-checking contextual equivalence of higher-order programs with references (candidat poste MCF)
by Guilhem Jaber from ENS Lyon/LIP Plume
Abstract: This talk will present SyTeCi, the first general automated tool to check contextual equivalence for programs written in an 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). As we will see, such examples can be found in many different programming languages.
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 transition systems 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, summarization 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.
