Domain-independent interprocedural program analysis using block-abstraction memoization

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.

BibTeX

@inproceedings{Beyer-Friedberger:FSE20,
  author    = {Dirk Beyer and
               Karlheinz Friedberger},
  title     = {Domain-independent interprocedural program analysis using block-abstraction memoization},
  booktitle = {{ESEC/SIGSOFT} {FSE}},
  pages     = {50--62},
  publisher = {{ACM}},
  year      = {2020},
}

Domain-independent interprocedural program analysis using block-abstraction memoization

Abstract

Related papers