KTH Demo: Proof Generation

Here you can download the producer-side tool (proof generator / packager) and a precompiled version of the consumer-side tool (verifier) in the form of a MIDlet.

The tools are in in pre-beta stage and no warranties are given whatsoever.

You can also download the prototype description report.

The Producer-side: Proof generator / packager

Download AnnotationGenerator.jar.

Required software

The tool depends on the following software:

• Sun JDK 1.5 or later (download page)
• Sun Java Wireless Toolkit for CLDC (download page)
• Our Inliner Tool (found at the other demo page)

Start the tool in the following way:

A screen shot of the program is found below:

The Consumer-side: Proof verifier

Download BCAV.jar and BCAV.jad.

Start the tool in the WTK emulator in the following way: