KTH Demo: Proof Generation

Overview

Online Demo
Load Java-source files
Compile class files
Inline class files
Preverify class files
Generate proof
Package into .jad/.jar
Verify policy adherence

Offline Demo
Download executable

Demo Videos
Developers Perspective
Users Perspective (fail)
Users Perspective (success)

This step loads the Java-source files into the working directory of the tool.

The online demo is hard-coded for the Worm-Game MIDlet files.

Tool output: 

Clearing content of working dir: wizard_workdir
COPYING GIVEN JAVA-SOURCE FILES INTO WORKING DIR...
    Copying wormgame/Worm.java to wizard_workdir/javafiles
    Copying wormgame/WormPit.java to wizard_workdir/javafiles
    Copying wormgame/WormMain.java to wizard_workdir/javafiles
    Copying wormgame/WormLink.java to wizard_workdir/javafiles
    Copying wormgame/WormFood.java to wizard_workdir/javafiles
    Copying wormgame/WormScore.java to wizard_workdir/javafiles
    Copying wormgame/ScoreSender.java to wizard_workdir/javafiles
    Copying wormgame/WormException.java to wizard_workdir/javafiles
DONE

View the source files here:

Proceed to next step: Compile class files >>