Enforcing termination of interprocedural analysis

Stefan Schulze Frielinghaus; Helmut Seidl; Ralf Vogler

doi:10.1007/978-3-662-53413-7_22

Enforcing termination of interprocedural analysis

Stefan Schulze Frielinghaus, Helmut Seidl, Ralf Vogler

Informatics 2 - Chair of Formal Languages, Compiler Construction, Software Construction

Technical University of Munich

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

5 Scopus citations

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.

Original language	English
Title of host publication	Static Analysis - 23rd International Symposium, SAS 2016, Proceedings
Editors	Xavier Rival
Publisher	Springer Verlag
Pages	447-468
Number of pages	22
ISBN (Print)	9783662534120
DOIs	https://doi.org/10.1007/978-3-662-53413-7_22
State	Published - 2016
Event	23rd International Symposium on Static Analysis, SAS 2016 - Edinburgh, United Kingdom Duration: 8 Sep 2016 → 10 Sep 2016

Publication series

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

Conference

Conference	23rd International Symposium on Static Analysis, SAS 2016
Country/Territory	United Kingdom
City	Edinburgh
Period	8/09/16 → 10/09/16

Access to Document

10.1007/978-3-662-53413-7_22

Cite this

Frielinghaus, S. S., Seidl, H., & Vogler, R. (2016). Enforcing termination of interprocedural analysis. In X. Rival (Ed.), Static Analysis - 23rd International Symposium, SAS 2016, Proceedings (pp. 447-468). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9837 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-662-53413-7_22

Frielinghaus, Stefan Schulze ; Seidl, Helmut ; Vogler, Ralf. / Enforcing termination of interprocedural analysis. Static Analysis - 23rd International Symposium, SAS 2016, Proceedings. editor / Xavier Rival. Springer Verlag, 2016. pp. 447-468 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{a166ab4ce5554a2f895ddca1f827d1e8,

title = "Enforcing termination of interprocedural analysis",

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.",

author = "Frielinghaus, {Stefan Schulze} and Helmut Seidl and Ralf Vogler",

note = "Publisher Copyright: {\textcopyright} Springer-Verlag GmbH Germany 2016.; 23rd International Symposium on Static Analysis, SAS 2016 ; Conference date: 08-09-2016 Through 10-09-2016",

year = "2016",

doi = "10.1007/978-3-662-53413-7_22",

language = "English",

isbn = "9783662534120",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "447--468",

editor = "Xavier Rival",

booktitle = "Static Analysis - 23rd International Symposium, SAS 2016, Proceedings",

}

Frielinghaus, SS, Seidl, H & Vogler, R 2016, Enforcing termination of interprocedural analysis. in X Rival (ed.), Static Analysis - 23rd International Symposium, SAS 2016, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 9837 LNCS, Springer Verlag, pp. 447-468, 23rd International Symposium on Static Analysis, SAS 2016, Edinburgh, United Kingdom, 8/09/16. https://doi.org/10.1007/978-3-662-53413-7_22

Enforcing termination of interprocedural analysis. / Frielinghaus, Stefan Schulze; Seidl, Helmut; Vogler, Ralf.
Static Analysis - 23rd International Symposium, SAS 2016, Proceedings. ed. / Xavier Rival. Springer Verlag, 2016. p. 447-468 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9837 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Enforcing termination of interprocedural analysis

AU - Frielinghaus, Stefan Schulze

AU - Seidl, Helmut

AU - Vogler, Ralf

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 -

Frielinghaus SS, Seidl H, Vogler R. Enforcing termination of interprocedural analysis. In Rival X, editor, Static Analysis - 23rd International Symposium, SAS 2016, Proceedings. Springer Verlag. 2016. p. 447-468. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-662-53413-7_22

Enforcing termination of interprocedural analysis

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this