salle A. Turing CE4
26 février 2015 - 14h00
Scalable Code Analysis with Policy Iteration
par George Karpenkov de VERIMAG
Abstract: We present a new algorithm for deriving numerical invariants
which combines the precision of max-policy iteration with the flexibility
and scalability of conventional Kleene iterations.
It is stated using Configurable Program Analysis
framework, thus allowing inter-analysis communication.
We augment the algorithm with adjustable block encoding, which gives better
results than the existing path focusing approach, and with a novel formula
slicing technique for precise alias analysis.
Our technique operates over any template linear constraint
domain; interval and octagon domains are emulated, and templates are
also derived from the program source.
The implementation is evaluated on a set of benchmarks from
the Software Verification Competition, and we obtain a competitive score with
state-of-the art analyzers.
