@inproceedings{10.1007/978-3-030-63461-2_24,
    Abstract = {We present a method for synthesizing loops over affine assignments from polynomial invariants. It is complete when the number of auxiliary variables is bounded, thus serving as a foundation for strength reduction optimization that convert polynomial expressions into incremental affine computations. Our work has applications towards synthesizing loops satisfying a given polynomial loop invariant, program verification, as well as generating number sequences from algebraic relations. To understand viability of the methodology and heuristics for synthesizing loops with a large number of auxiliary variables, we implement and evaluate the method using the Absynth tool.},
    Address = {Cham},
    Author = {Humenberger, Andreas and Bj{\o}rner, Nikolaj and Kov{\'a}cs, Laura},
    BookTitle = {Integrated Formal Methods},
    Editor = {Dongol, Brijesh and Troubitsyna, Elena},
    File = {Algebra-Based Loop Synthesis - 10.1007@978-3-030-63461-2 - h - h.pdf},
    ISBN = {978-3-030-63461-2},
    Pages = {440--459},
    Publisher = {Springer International Publishing},
    Title = {Algebra-Based Loop Synthesis},
    Year = {2020},
    date-added = {2021-03-29 14:48:19 +0200},
    date-modified = {2021-03-29 14:48:19 +0200},
    doi = {10.1007/978-3-030-63461-2_24}
}

@inproceedings{10.1007/978-3-030-63461-2_24, Abstract = {We present a method for synthesizing loops over affine assignments from polynomial invariants. It is complete when the number of auxiliary variables is bounded, thus serving as a foundation for strength reduction optimization that convert polynomial expressions into incremental affine computations. Our work has applications towards synthesizing loops satisfying a given polynomial loop invariant, program verification, as well as generating number sequences from algebraic relations. To understand viability of the methodology and heuristics for synthesizing loops with a large number of auxiliary variables, we implement and evaluate the method using the Absynth tool.}, Address = {Cham}, Author = {Humenberger, Andreas and Bj{\o}rner, Nikolaj and Kov{\'a}cs, Laura}, BookTitle = {Integrated Formal Methods}, Editor = {Dongol, Brijesh and Troubitsyna, Elena}, File = {Algebra-Based Loop Synthesis - 10.1007@978-3-030-63461-2 - h - h.pdf}, ISBN = {978-3-030-63461-2}, Pages = {440--459}, Publisher = {Springer International Publishing}, Title = {Algebra-Based Loop Synthesis}, Year = {2020}, date-added = {2021-03-29 14:48:19 +0200}, date-modified = {2021-03-29 14:48:19 +0200}, doi = {10.1007/978-3-030-63461-2_24} }