Deaccumulation - Improving Provability

Authors: J. Giesl, A. Kühnemann, and J. Voigtländer
Published: In 8th Asian Computing Science Conference (ASIAN'03, acceptance rate 16/53), Mumbai, India, Proceedings, volume 2896 of LNCS, pages 146-160, Springer, December 2003.
DOI: 10.1007/978-3-540-40965-6_10
BibTeX: GKV03.bib
Abstract: Several induction theorem provers were developed to verify functional programs mechanically. Unfortunately, automated verification usually fails for functions with accumulating arguments. In particular, this holds for tail-recursive functions that correspond to imperative programs, but also for programs with nested recursion. Based on results from the theory of tree transducers, we develop an automatic transformation technique. It transforms accumulative functional programs into non-accumulative ones, which are much better suited for automated verification by induction theorem provers. Hence, in contrast to classical program transformations aiming at improving the efficiency, the goal of our deaccumulation technique is to improve the provability.
Download: DeaccumulationImprovingProvability.pdf
Rights: Copyright held by Springer.

An extended version of this work appeared in Journal of Logic and Algebraic Programming, see here.