VeriWeb is a web-based IDE for verification that decomposes the task of writing verifiable specifications into manageable subproblems.
VeriWeb users write Java Modeling Language (JML) specifications which are verified using the Extended Static Checker for Java version 2 (ESC/Java2).
The VeriWeb interface is described in the paper Reducing the barriers to writing verified specifications which was presented at the OOPSLA 2012 conference.
The study results can be found on the project page. These will eventually be moved to this repository.
VeriWeb is not under active development. This repository contains the latest snapshot of the VeriWeb development source code from our local repository. As such, the code may differ in certain places from the description in the publication. Known differences are:
- Mechanical Turk doesn't work in this version of the code.
- Object invariant inference and handling
If you'd like to try building and running VeriWeb, please contact me. The basic instructions are:
- Deploy and run the verification server
- Deploy VeriWeb via Apache Tomcat
In practice, the server requires a very specific directory structure which I haven't gotten around to documenting yet.
Because VeriWeb uses ESC/Java2 under the hood, it only supports Java 1.4 programs. I created an Eclipse plug-in to automatically convert Java 1.5 and 1.6 projects to Java 1.4.
This software is licensed under Matt Might's wonderful CRAPL academic license.
This software is based upon work supported by the National Science Foundation Graduate Research Fellowship under Grant No. DGE-0718124.