The goal of WAVE is the Specification and Verification of Interactive Web Applications powered by an underlying database. WAVE allows web application developers to declaratively specify the behavior of an interactive web application as a function of the user input, the current state of the application, and the information in an underlying database.


Desirable properties of the web application can be specified using temporal logic and verified statically, at design time.


The current version of WAVE has the following modules:

The Verifier takes as inputs the specification of a Web application and a property, and outputs whether the property is true or false for that Web application together with plenty of useful verification information (such as a counterexample in case of a false property).


Interactive web applications have emerged as a major paradigm for publishing information on the Internet. These applications are increasingly complex, requiring static analysis tools for boosting the confidence in their robustness and correctness and for enhancing their functionality and efficiency.


This is a joint collaboration of the University of California, San Diego and the San Diego Supercomputer Center.

The Demo

This demo illustrates our framework for web application specification. In the future, the demo will be extended to illustrate the automatic generation of web applications from specifications, and the verification of properties.


This material is based upon work supported by the National Science Foundation under Grant No. 0415257.

Disclaimer: Any opinions, findings and conclusions or recomendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the National Science Foundation (NSF).