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

Description of the characteristics of the transition systems:

• The rectangle 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.