IMAG 206
30 mars 2017 - 14h00
Enforcing Termination of Interprocedural Analysis
par Helmut Seidl de Technische Universitaet Muenchen
30 mars 2017 - 14h00
Enforcing Termination of Interprocedural Analysis
par Helmut Seidl de Technische Universitaet Muenchen
Abstract: Interprocedural analysis by means of partial tabulation of summary
functions may not terminate when the same procedure is analyzed for
infinitely many abstract calling contexts or when the abstract domain
has infinite strictly ascending chains.
As a remedy, we present a novel local solver for general abstract
equation systems, be they monotonic or not, and prove that this solver
fails to terminate only when infinitely many variables are encountered.
We clarify in which sense the computed results are sound.
Moreover, we show that interprocedural analysis performed by this novel
local solver, is guaranteed to terminate for all non-recursive programs
- -- irrespective of whether the complete lattice is infinite or has
infinite strictly ascending or descending chains.
