This is a web interface to the Interproc analyzer connected to the APRON Abstract Domain Library and the Fixpoint Solver Library, whose goal is to demonstrate the features of the APRON library and, to a less extent, of the Analyzer fixpoint engine, in the static analysis field.
There are two compiled versions: interprocweb, in which all the abstract domains use underlying multiprecision integer/rational numbers, and interprocwebf, in which box and octagon domains use underlying floating-point numbers in safe way.
This is the Interproc version
Here are some program examples: incr ackerman fact numerical numerical2 maccarthy91 heapsort symmetricalstairs
In order not to flood our web-server, analysis computation time is limited to 1min in this demonstration. Also note that result files are temporary files stored on our server that have a very short life-time.
The analysis computes an invariant at each program point.
The Interproc is freely available. It is written in C, with a OCaml binding. The APRON Abstract Domain Library analyzer and the Fixpoint Solver Library are freely available, and are written in OCaml.
This CGI-WEB interface is written in OCaml using the OCamlHtml library, freely available