5 mars 2018
Guilhem Jaber (ENS-Lyon)This talk will present SyTeCi, the first general automated tool to prove contextual equivalence for programs written in an higher-order language with references (i.e. local mutable states).
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. In fact, contextual equivalence is undecidable, even in a finitary setting (finite datatypes, no recursion).
Then, we will introduce SyTeCi, a sound tool to automatically prove such equivalences. This tool is based on a reduction of the problem of contextual equivalence of two programs to the problem of non-reachability in transition systems of memory configurations.
This reduction is based on the generation, from two programs P1,P2, of a “characteristic formula” F, written in a temporal logic. We have that F is satisfiable w.r.t. such a transition system iff P1,P2 are contextually equivalent.
Contextual equivalence being undecidable, so does the non-reachability problem. However, one can apply model-checking techniques (predicate abstraction, summarization of pushdown systems) to check non-reachability via approximations. This allows to prove automatically many non-trivial examples of the literature, that could only be proved by hand before.