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.