research-article

Open access

Domain-independent interprocedural program analysis using block-abstraction memoization

Authors:

Karlheinz FriedbergerAuthors Info & Claims

ESEC/FSE 2020: Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering

Pages 50 - 62

https://doi.org/10.1145/3368089.3409718

Published: 08 November 2020 Publication History

PDF eReader

Abstract

Whenever a new software-verification technique is developed, additional effort is necessary to extend the new program analysis to an interprocedural one, such that it supports recursive procedures. We would like to reduce that additional effort. Our contribution is an approach to extend an existing analysis in a modular and domain-independent way to an interprocedural analysis without large changes: We present interprocedural block-abstraction memoization (BAM), which is a technique for procedure summarization to analyze (recursive) procedures. For recursive programs, a fix-point algorithm terminates the recursion if every procedure is sufficiently unrolled and summarized to cover the abstract state space.

BAM Interprocedural works for data-flow analysis and for model checking, and is independent from the underlying abstract domain. To witness that our interprocedural analysis is generic and configurable, we defined and evaluated the approach for three completely different abstract domains: predicate abstraction, explicit values, and intervals. The interprocedural BAM-based analysis is implemented in the open-source verification framework CPAchecker. The evaluation shows that the overhead for modularity and domain-independence is not prohibitively large and the analysis is still competitive with other state-of-the-art software-verification tools.

Supplementary Material

Auxiliary Teaser Video (fse20main-p384-p-teaser.mp4)

We present interprocedural block-abstraction memoization (BAM Interprocedural), which a technique for procedure summarization to analyze (recursive) procedures. For recursive programs, a fix-point algorithm terminates the recursion if every procedure is sufficiently unrolled and summarized to cover the abstract state space. The analysis is implemented in the open-source verification framework CPAchecker. The evaluation shows that the overhead for modularity and domain-independence is not prohibitively large and the analysis is still competitive with other state-of-the-art software-verification tools.

Download
3.83 MB

Auxiliary Presentation Video (fse20main-p384-p-video.mp4)

Download
32.98 MB

References

[1]

A. Albarghouthi, A. Gurfinkel, and M. Chechik. 2012. Whale: An InterpolationBased Algorithm for Inter-procedural Verification. In Proc. VMCAI (LNCS 7148). Springer, 39-55. https://doi.org/10.1007/978-3-642-27940-9_4

Abstract

Supplementary Material

References

Cited By

Index Terms

Recommendations

Interprocedural pointer alias analysis

Evaluating the benefits of context-sensitive points-to analysis using a BDD-based implementation

Interprocedural Probabilistic Pointer Analysis

Comments

Information

Published In

Sponsors

Publisher

Publication History

Permissions

Check for updates

Badges

Author Tags

Qualifiers

Funding Sources

Conference

Acceptance Rates

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

PDF

eReader

Login options

Full Access

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations