The ConcurInterproc Analyzer

This is a web interface to the ConcurInterproc analyzer connected to the BDDAPRON and the Fixpoint Solver Library.

Arguments

Please type a program, upload a file from your hard-drive, or choose one the provided examples:

Hit the OK button to proceed:

Program source: scheduling policy Inlining (`all', or comma-separated list of proc. names)

Kind of Analysis:
sequence of forward and backward analysis
Abstract Domains:
Numerical Logico-Numerical

Iterations/Widening options:
dynamic CFG exploration (concurrent programs) guided iterations threshold inference and analysis with them
widening delay descending steps

Results options:
Print bounding boxes
Project on thread Keep frozen variables Keep information about other threads

``Simple'' language syntax

Benchmarks

Here are other program examples: incrr maccarthy91 maccarthy91b heapsort symmetricalstairs numerical finitetype barrier_counter Peterson mutual exclusion Kessel mutual exclusion BlueToothQadeerWu_PLDI2004 QuadeerRajamaniRehof_POPL04

Results

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.

Informations

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

Bertrand Jeannet
bjeannet@NOSPAM inrialpes.fr