Understanding Proof Attempts Evaluation

The goal of the evaluation is to compare the inspection of proof attempts using KeY and the Symbolic Execution Debugger (SED). The evaluation is realized as part of Eclipse and fully self explaining. During the evaluation you can enjoy nice introduction videos about the tools and test your knowledge while answering questions about four proof attempts. Knowledge about KeY and JML is helpful but not required. The evaluation usually takes about 60 minutes.

Participation (Installation)

Please follow the steps to participate in the evaluation:

1. Install prerequisites:
   • Java 7 or newer
   • libwebkitgtk (Linux only)
     sudo apt-get install libwebkitgtk-1.0-0
2. Ensure that your firewall allows access to sed.se.informatik.tu-darmstadt.de on port 10947.
3. Download the best matching preconfigured Eclipse Luna product. It contains all required features:
   • aix (gtk/ppc)
   • aix (gtk/ppc64)
   • hpux (gtk/ia64)
   • linux (gtk/ppc)
   • linux (gtk/ppc64)
   • linux (gtk/ppc64le)
   • linux (gtk/s390)
   • linux (gtk/s390x)
   • linux (gtk/x86)
   • linux (gtk/x86_64)
   • macosx (cocoa/x86)
   • macosx (cocoa/x86_64)
   • solaris (gtk/sparc)
   • solaris (gtk/x86)
   • win32 (win32/x86)
   • win32 (win32/x86_64)
4. Extract the downloaded ZIP archive (e.g. into a temporary directory).
5. Start the executable file SED of folder SED.
   1. Use an empty workspace.
   2. Select main menu item Evaluation, Understanding Proof Attempts and finish the opened wizard.
6. After finishing the evaluation the extracted folder SED (and the used workspace) can be deleted.

Useful Hints for the Evaluation

• Follow the mentioned best practices.
• Do not try to understand the full proof attempt at once, focus on one goal/problem at a time.
• Watch the instruction videos again, if usage of the tools is unclear.
  (Previously shown instructions are available in the bottom toolbar of the evaluation wizard.)
• Do not spend much more than 10 minutes per proof attempt. If you don't understand the proof attempt, feel free to select the 'I tried my best' option.

Contact

If you have any questions, feel free to contact Martin Hentschel (hentschel@cs.tu-darmstadt.de).

Screenshot

The following screenshot shows the evaluation wizard: