CMP.13:7 - Conformance Checklist

• The initial possibilities, transitions and requested observation identify the computation being analyzed.
• Each abstract value has an interpretation, and the inference direction supports the claimed conclusion.
• Abstract operations and joins cover their original counterparts; the obtaining algorithm has a justified completion or bounded-result condition.
• A whole-reachability conclusion uses initial containment and transition closure.
• A claimed concrete counterexample has a consecutive realization; a failed reconstruction identifies the lost distinction or remaining uncertainty.
• Refinement preserves the original possibilities and changes a result relevant to the receiving work.