Deaccumulation techniques for improving provability Export

@article{citeulike:1410394, 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.}, author = {Giesl, J\"{u}rgen and K\"{u}hnemann, Armin and Voigtl\"{a}nder, Janis}, citeulike-article-id = {1410394}, citeulike-linkout-0 = {http://www.sciencedirect.com/science/article/B6W8D-4MS9JMK-1/2/4d31a58ded4f30401be24c46460e9c65}, citeulike-linkout-1 = {http://dx.doi.org/10.1016/j.jlap.2006.11.001}, citeulike-linkout-2 = {http://wwwtcs.inf.tu-dresden.de/~voigt/Deaccumulation.pdf}, doi = {10.1016/j.jlap.2006.11.001}, journal = {Journal of Logic and Algebraic Programming}, keywords = {accumulating-parameters, functional-programming, induction-proofs, program-transformation, theorem-provers, tree-transducers, verification}, month = {April}, number = {2}, pages = {79--113}, posted-at = {2007-06-25 11:31:13}, priority = {0}, title = {Deaccumulation techniques for improving provability}, url = {http://dx.doi.org/10.1016/j.jlap.2006.11.001}, volume = {71}, year = {2007} }

TY - JOUR ID - citeulike:1410394 L3 - citeulike-article-id:1410394 N2 - 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. IS - 2 JF - Journal of Logic and Algebraic Programming EP - 113 TI - Deaccumulation techniques for improving provability VL - 71 SP - 79 KW - accumulating-parameters KW - functional-programming KW - induction-proofs KW - program-transformation KW - theorem-provers KW - tree-transducers KW - verification AU - Giesl, Jürgen AU - Kühnemann, Armin AU - Voigtländer, Janis PY - 2007/04// UR - http://dx.doi.org/10.1016/j.jlap.2006.11.001 ER -