VeriWeb: Reducing the barriers to formal methods

VeriWeb is a web-interface for verifying Java programs with ESC/Java2. It introduces several innovative features to lower the skill barrier to formal verification and enable crowdsourced verification.

VeriWeb and related technologies are currently developed by Todd Schiller, Kellen Donohue, Forrest Coward, Allen Liu, and Michael Ernst.

License: All content and data on this page is currently licensed under Matt Might's fine CRAPL academic license.

Source Code

The VeriWeb source code is available on Github under the CRAPL academic license.

Live Demo

The demo server is currently down; if you need access to a live demo or demo video please email Todd Schiller.

Caveat emptor: The demo server is running the development version of VeriWeb. Currently this means:

If VeriWeb crashes or freezes, refresh the page
The demo is running on a Rackspace with a small amount of RAM; verification may be slow when checking multiple conditions simultaneously.
VeriWeb works best with Chrome or Firefox since it uses Google Web Toolkit. Some of the features will not work in certain versions of Internet Explorer.
Collaborative verification is not available in the demo right now. Check back soon as we will be adding support for creating collaborative sessions.
We're currently playing around with object invariant inference and handling. Among other things, this means that the tutorial included in the vWorker materials for the FixedSizeSet project may not be exactly correct.

Study Materials and Results

Comparative Study Materials

vWorker project posting
Bid summary (OpenDocument Spreadsheet)
StackAr method dependency graph
Source Files: StackAr.java (ADT) and StackArCheck.java (client class)
Eclipse instructions and tutorial
VeriWeb instructions and tutorial

Comparative Study Results

We will be releasing combined bid, performance, and survey results once we have a chance to merge and anonymize the data. Full session logs will be released with the VeriWeb source, as they are in a custom binary format.

Bid summary (OpenDocument Spreadsheet)
Raw Questionnaire Results (OpenDocument Spreadsheet). Excel handles the vertical height of the cells better than OpenOffice; exporting to HTML also works fairly well.
Full Eclipse session logs: coming soon. Includes all edits and ESC/Java2 invocations.
Full VeriWeb session logs: coming soon. Includes all VeriWeb actions.

Collaborative Study Materials

QueueAr method dependency graph
Source Files: QueueAr.java (ADT) and QueueArCheck.java (client class)

This material is based upon work supported by the National Science Foundation Graduate Research Fellowship under Grant No. DGE-0718124.