@inproceedings{DBLP:conf/popl/HeizmannHP10,
  author    = {Matthias Heizmann and Jochen Hoenicke and Andreas Podelski},
  title     = {Nested interpolants},
  booktitle = {POPL},
  year      = {2010},
  pages     = {471-482},
  subproject = {R1},
  access    = {restricted},
  bibtex    = {heizmann.popl10.bib},
  pdf       = {heizmann.popl10.pdf},
  abstract  = {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).},
}