@inproceedings{HH12,
title = { When the decreasing sequence fails },
author = {Halbwachs, Nicolas and Henry, Julien},
month = {sep},
year = {2012},
booktitle = {19th International Static Analysis Symposium, SAS'12},
address = {Deauville, France},
pages = {198--213},
publisher = {LNCS 7460, Springer Verlag},
team = {SYNC},
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.
},
}
