Write a Blog >>
Thu 12 Nov 2020 08:30 - 08:32 at Virtual room 1 - Analysis 4

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.

Thu 12 Nov
Times are displayed in time zone: (UTC) Coordinated Universal Time change

08:30 - 09:00
08:30
2m
Talk
Domain-Independent Interprocedural Program Analysis using Block-Abstraction Memoization
Research Papers
Dirk BeyerLMU Munich, Germany, Karlheinz FriedbergerLMU Munich, Germany
DOI Pre-print Media Attached
08:33
1m
Talk
Inherent Vacuity for GR(1) Specifications
Research Papers
Shahar MaozTel Aviv University, Israel, Rafi ShalomTel Aviv University, Israel
DOI
08:35
1m
Talk
Interval Counterexamples for Loop Invariant Learning
Research Papers
Rongchen XuTsinghua University, China, Fei HeTsinghua University, Bow-Yaw WangAcademia Sinica
DOI
08:37
1m
Talk
Modular Collaborative Program Analysis in OPAL
Research Papers
Dominik HelmTU Darmstadt, Germany, Florian K├╝blerTU Darmstadt, Germany, Michael ReifTU Darmstadt, Germany, Michael EichbergTU Darmstadt, Germany, Mira MeziniTU Darmstadt, Germany
DOI
08:39
1m
Talk
Past-Sensitive Pointer Analysis for Symbolic Execution
Research Papers
David TrabishTel Aviv University, Israel, Timotej KapusImperial College London, UK, Noam RinetzkyTel Aviv University, Cristian CadarImperial College London, UK
DOI Pre-print Media Attached
08:41
19m
Talk
Conversations on Analysis 4
Paper Presentations
David TrabishTel Aviv University, Israel, Dominik HelmTU Darmstadt, Germany, Rafi ShalomTel Aviv University, Israel, Rongchen XuTsinghua University, China, Shahar MaozTel Aviv University, Israel, M: Rachel Tzoref-BrillIBM Research