Enforcing termination of interprocedural analysis

Stefan Schulze Frielinghaus, Helmut Seidl, Ralf Vogler

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

5 Scopus citations


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.

Original languageEnglish
Title of host publicationStatic Analysis - 23rd International Symposium, SAS 2016, Proceedings
EditorsXavier Rival
PublisherSpringer Verlag
Number of pages22
ISBN (Print)9783662534120
StatePublished - 2016
Event23rd International Symposium on Static Analysis, SAS 2016 - Edinburgh, United Kingdom
Duration: 8 Sep 201610 Sep 2016

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume9837 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference23rd International Symposium on Static Analysis, SAS 2016
Country/TerritoryUnited Kingdom


Dive into the research topics of 'Enforcing termination of interprocedural analysis'. Together they form a unique fingerprint.

Cite this