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.