This page demonstrates the method described in the article Inferring Sufficient Conditions with Backward Polyhedral Under-Approximations accepted to NSAD 2012.
On this page, you can supply a program to be analyzed by our proof-of-concept prototype analyzer, run on our web-server. Too avoid flooding the servers, the analyzer rejects programs that are too large or feature too many variables, and timeouts after a few seconds.
The source code of the analyzer is also available for download under the CRAPL license. Please see the READ ME file from the distribution.
In case of issue, please contact mine at di.ens.fr.
Disclaimer: This prototype is a proof-of-concept for experimental research ideas and in an early stage of development. It may contain bugs and may fail to work as intended.
The analysis consists in two phases: a forward over-approximating analysis, followed by a backward under-approximating analysis.
Both analyses proceed by structural induction on the program syntax, evaluating instructions in the abstract domain, stepping into functions (full context-sensitivity), and iterating loops until an abstract fix-point is reached (in case of nested loops, the inner loop is re-analyzed for each iteration of the outer loop, following Bourdoncle's recursive iteration strategy).
The forward analysis computes, at each program point, an invariant. It is an over-approximation of the set of environments that can be reached at these program points by the set of all possible executions. If an execution violates an assertion, then only the environments before the assertion is encountered contribute to the invariant. The result of the forward analysis is (an over-approximation of) the set of environments when executions reach the end of the program without violating any assertion.
The backward analysis computes, at each program point, a sufficient condition so that all executions that obey this condition each time they reach this point will never violate any assertion (but do not necessarily terminate). It computes an under-approximation. The result of the backward analysis is a sufficient condition at the beginning of the program for the program to never violate any assertion, whatever the non-deterministic choices taken during the execution.
The abstract domain considered is that of convex closed polyhedra, as introduced by Cousot and Halbwachs and enriched with backward under-approximating operators. It is implemented on top of the Apron library. The analyzer is written in OCaml form scratch.