Nested interpolants

12 years 6 months ago
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...
Matthias Heizmann, Jochen Hoenicke, Andreas Podels
Added 06 Dec 2010
Updated 06 Dec 2010
Type Conference
Year 2010
Where POPL
Authors Matthias Heizmann, Jochen Hoenicke, Andreas Podelski
Comments (0)