SyTeCi: Model-checking contextual equivalence
of higher-order programs with references
Description of the characteristics of the transition systems:
- The doubled circle state is the initial state.
- The diamond states are the failed states.
- Blue transitions correspond to transitions taken by the two programs (i.e. by Player), while red ones correspond to transitions taken by the environment (i.e. by Opponent).
- Dotted transitions correspond to epsilon transitions.
- Each Player transition is labelled by:
- a description of the modification of the heap by the first and by the second program (indicated by h1 ↝ h2, where h1,h2 are two symbolic heaps, with ε indicating the empty heap);
- a set of arithmetic constraints on the variables appearing in the symbolic heaps and in the terms;
- a tag indicating what kind of transition it is:
- Player Internal (PI), that corresponds to an evaluation to recursive calls;
- Player Question (PQ), that corresponds to the call of a function provided by the environment (i.e. a callback);
- Player Answer (PA), that corresponds to the evaluation to a (possibly higher-order) value.
- Each Opponent transition is labelled by a tag indicating what kind of transition it is:
- Opponent Question (OQ), that corresponds to the call of a function provided by the program;
- Opponent Answer (OA), that corresponds to the answer of a callback.