Web Interface for Verification Tools

The great overwhelming of prototype tools developed within research projects suffers from several limitations and requirements preventing their usability, such as, for example, a particular version of compiler, dependencies to other tools previously installed and correctly configured, machine with a particular hardware configuration, etc. Goal of the project is to develop a platform allowing the human interaction with tools through a web interface, overcoming to all the aforementioned limitations to their usability and spread.

To make things ever worse, new version of prototype tools are likely to be released within small periods of time (bug fixing, new features, heuristics, etc.), and most likely there is no time to test if the new version works for every combination of operating system, hardware, libraries, compilers, etc.

The amount of time needed to fix dependecies problems or create a solid interface might be too much and out of scope of research, which main goal is to show that a new idea works, not to sell a fancy product.

 

A side effect of this problem comes with tools that comes with research papers. Papers usually comes with an experimental section where algorithms and heuristics described previously have been implemented and tested with a prototype. The tool might be available for download to the reviewer, but most likely only as binaries (suffering from the aforementioned problems).

 

The goal of this project is to develop a platform that would alleviate the burden of releasing new tools: this platform will have a web interface, and the developer will provide a machine on which this platform will run. This way, everyone who is interested in its tool can play with the tool through the web interface.

 

Moreover, this platform would provide a good way to give live demos at conferences or talks, giving to the audience the chance to try on-line the new tool, providing immediate feedback and suggestions.

 

The new platform will be built in Python and tested with SAFARI, a newborn invariant generator/infinite-state model checker.

 

The project will be carried out mainly under the supervision and support of Francesco Alberti (http://www.inf.usi.ch/phd/alberti/), SAFARI's main developer and maintainer, and Prof. Natasha Sharygina (http://www.inf.usi.ch/faculty/sharygina/). Other memembers of the Software verification an security lab (http://verify.inf.usi.ch) will provide feedbacks and benchmarks.

 

- web programming

- knowledge of Python and previous experience with multi-thread programming are a plus

 

- solid and deep knowledge of Python (why Python? http://www.python.org/about/quotes/)

- solid and deep competencies in multi-thread programming