Auditorium (IMAG)
27 avril 2017 - 13h30
Finding Inductive Invariants using SMT Solving and Convex Optimization
par George Karpenkov de VERIMAG
Abstract: Static analysis concerns itself with deriving program properties which hold
universally for all program executions.
Such properties are used for proving program properties (e.g. there never
occurs an overflow or other runtime error regardless of a particular execution) and are almost
invariably established using inductive invariants: properties which hold
for the initial state and imply themselves under the program transition, and thus
hold universally due to induction.
A traditional approach for finding numerical invariants is using abstract
interpretation, which can be seen as interpreting the program in the abstract
domain of choice, only tracking properties of interest.
Yet even in the intervals abstract domain (upper and lower bounds
for each variable) such computation does not necessarily converge, and the
analysis has to resort to the use of widenings to enforce
convergence at the cost of precision.
An alternative game-theoretic approach called policy iteration,
guarantees to find
the least inductive invariant in the chosen abstract domain under the finite
number of iterations.
Yet the original description of the algorithm includes a number of drawbacks:
it requires converting the entire program to an equation system,
does not integrate with other approaches,
and is unable to benefit from other analyses.
Our new algorithm for running local policy iteration (LPI)
instead formulates policy iteration as traditional Kleene iteration,
with a widening operator that guarantees to return the least inductive
invariant in the domain after finitely many applications.
Local policy iteration runs in template linear constraint domains which
requires setting in advance the ``shape'' of the derived invariant (e.g.
$x + 2y$ for deriving $x + 2y leq 10$).
Our second theoretical contribution involves development and comparison of
a number of different template synthesis strategies, when used in conjunction
with LPI.
Additionally, we present an approach for generating abstract reachability
trees using abstract interpretation,
enabling the construction of counterexample traces,
which in turns lets us generate new templates using Craig interpolants.
In our third contribution we bring our attention to interprocedural and
potentially recursive programs.
We develop an algorithm parameterizable with any abstract interpretation for
summary generation, and we study it's parameterization with LPI.
The resulting approach is able to generate least inductive invariants in the domain for a fixed number of summaries for recursive programs.
Our final theoretical contribution is a novel formula slicing''
method for finding potentially disjunctive inductive invariants
from program fragments obtained by symbolic execution.
We implement all of these techniques in the open-source state-of-the-art
CPAchecker program analysis framework, enabling communication and collaboration
between different analyses.
The techniques mentioned above rely on
satisfiability modulo theories solvers,
which are capable of
giving solutions to
first-order formulas over certain theories or showing
that none exists.
In order to simplify communication with such tools
we present the JavaSMT library, which provides a generic interface for such
communication.
The library has shown itself to be a valuable tool, and is already used by many
researchers.
Second defense rehearsal
