Nested interpolants

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 icate 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 onstruction 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). Categories and Subject Descriptors D.2.4 [Software Engineering]: Software/Program Verification; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs General Terms Languages, Theory, Verification. Keywords Nested words, interpolants, recursion, static analysis, abstract interpretation, software...

• Type: Conference
• Year: 2010
• Where: POPL
• Authors: Matthias Heizmann, Jochen Hoenicke, Andreas Podelski
• Keywords: Nested Word, Nested Word Automaton, POPL 2010, Programming Languages, Recursive Programs