This is a web interface to the ConcurInterproc analyzer connected to the BDDAPRON and the Fixpoint Solver Library.
Here are other program examples: incrr maccarthy91 maccarthy91b heapsort symmetricalstairs numerical finitetype barrier_counter Peterson mutual exclusion Kessel mutual exclusion BlueToothQadeerWu_PLDI2004 QuadeerRajamaniRehof_POPL04
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 ConcurInterproc is freely available. It is written in C, with a OCaml binding. The APRON Numerical Abstract Domains 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