Nested Interpolants

作者：Heizmann Matthias^*; Hoenicke Jochen; Podelski Andreas

来源：ACM Sigplan Notices, 2010, 45(1): 471-482.

DOI：10.1145/1707801.1706353

• Languages
• Theory
• Verification
• Nested words
• interpolants
• recursion
• static analysis
• abstract interpretation
• software model checking
• abstraction refinement
• Floyd-Hoare logic

In this paper, we explore the potential of the theory of nested words for partial correctness proofs of recursive programs. Our conceptual contribution is a simple framework that allows us to shine a new light on classical concepts such as Floyd/Hoare proofs and predicate abstraction in the context of recursive programs. Our technical contribution is an interpolant-based software model checking method for recursive programs. The method avoids the costly construction of the abstract transformer by constructing a nested word automaton from an inductive sequence of 'nested interpolants' (i.e., interpolants for a nested word which represents an infeasible error trace).

• 出版日期2010-1