salle A. Turing CE4
11 March 2014 - 15h45
When the decreasing sequence fails...
by Nicolas Halbwachs from Verimag
Abstract: The classical method for program analysis by abstract interpretation
consists in computing a increasing sequence with widening, which
converges towards a correct solution, then computing a decreasing
sequence of correct solutions without widening. It is generally
admitted that, when the decreasing sequence reaches a fixpoint,
it cannot be improved further. As a consequence, all efforts
for improving the precision of an analysis have been devoted to
improving the limit of the increasing sequence. In this paper,
we propose a method to improve a fixpoint after its computation.
The method consists in projecting the solution onto well-chosen
components and to start again increasing and decreasing sequences
from the result of the projection.
