| Authors: |
J. Giesl, A. Kühnemann, and J. Voigtländer |
| Published: |
Journal of Logic and Algebraic Programming, volume 71(2), pages 79-113, Elsevier, 2007. |
| DOI: |
10.1016/j.jlap.2006.11.001 |
| BibTeX: |
GKV07.bib |
| Abstract: |
Several induction theorem provers were developed to verify
functional programs mechanically. Unfortunately, automatic
verification often fails for functions with accumulating arguments.
Using concepts from the theory of tree transducers and extending
on earlier work, the paper develops automatic transformations from
accumulative functional programs into non-accumulative ones, which
are much better suited for mechanized verification. The overall
goal is to reduce the need for generalizing induction hypotheses in
(semi-)automatic provers. Via the correspondence between imperative
programs and tail-recursive functions, the presented approach can
also help to reduce the need for inventing loop invariants in the
verification of imperative programs.
|
| Download: |
DeaccumulationTechniquesForImprovingProvability.pdf |
| Rights: |
Copyright held by Elsevier. The definitive version of this work is available from http://dx.doi.org/10.1016/j.jlap.2006.11.001. |