SED

Please watch the introduction video (no audio). You can pause the video at any time to comprehend the content.

Best Practices

  1. Focus on an unverified node indicated by a red cross.
    1. Inspect the parent nodes to comprehend the followed execution path.
    2. Comprehend the truth values of the unverified node to identify what could not be shown.
    3. Inspect the symbolic state to identify bugs. If there is none, the proof can be closed interactively outside of SED.