TY - GEN
T1 - Enforcing termination of interprocedural analysis
AU - Frielinghaus, Stefan Schulze
AU - Seidl, Helmut
AU - Vogler, Ralf
N1 - Publisher Copyright:
© Springer-Verlag GmbH Germany 2016.
PY - 2016
Y1 - 2016
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84988423960&partnerID=8YFLogxK
U2 - 10.1007/978-3-662-53413-7_22
DO - 10.1007/978-3-662-53413-7_22
M3 - Conference contribution
AN - SCOPUS:84988423960
SN - 9783662534120
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 447
EP - 468
BT - Static Analysis - 23rd International Symposium, SAS 2016, Proceedings
A2 - Rival, Xavier
PB - Springer Verlag
T2 - 23rd International Symposium on Static Analysis, SAS 2016
Y2 - 8 September 2016 through 10 September 2016
ER -