SED

Please watch the introduction video (no audio). You can pause the video at any time to comprehend the content. Click here, if you want to open the example of the video in SED (Eclipse).

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.