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 and predicate abstraction in the context...

Full description

Saved in:
Bibliographic Details
Published in:ACM SIGPLAN notices 2010-01, Vol.45 (1), p.471-482
Main Authors: HEIZMANN, Matthias, HOENICKE, Jochen, PODELSKI, Andreas
Format: Article
Language:English
Subjects:
Applied sciences
Computer science
control theory
systems
Computer systems performance. Reliability
Exact sciences and technology
Software
Software engineering
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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).
ISSN:1523-2867
0362-1340
1558-1160
DOI:10.1145/1707801.1706353