一句话：提出 BAM 方法，以模块化、领域无关方式将现有分析扩展为支持递归的过程间分析。
每当提出新的软件验证技术，若要让其支持递归过程，通常还需额外工作把分析扩展为过程间分析。本文旨在降低这类额外工作量，提出过程间块抽象记忆化（BAM），一种领域无关且模块化的过程摘要技术。它无需对已有分析做大幅修改，即可将现有分析扩展为过程间分析。对于递归程序，BAM 使用不动点算法，当每个过程都被充分展开并总结到足以覆盖抽象状态空间时终止递归。该工作强调模块化与领域无关性，使分析开发者能以较小代价获得过程间能力；摘要未报告具体实现或实验评估。
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.