Javanni: A JavaScript Verifier

Overview

JavaScript is one of the most widely used programming language for the web, however, its dynamic typing makes JavaScript programs error-prone. Javanni is a verifier for JavaScript. It proves the absence of common programming errors such as reading an undefined field, and invoking a function with the wrong number of arguments. Javanni also proves functional correctness properties by adding assertions to the JavaScript program. Our case study using several JavaScript programs suggest that tools for dynamic typed languages can be used not only to prove functional correctness, but also to detect type errors or prove their absence.

The tool

Javanni is integrated in CloudStudio (a cloud-based IDE). Click here to try the Javanni verifier. Use the username "real" and password "madrid".

Demo

Watch it in YouTube here

Examples

You can find the source code of the examples used in a case study here , or log in into CloudStudio using the username "real" and password "madrid", and open the project "demoJavaScript".

Project Members

Martin Nordio
Cristiano Calcagno
Carlo Furia