@inproceedings{Kovacs:ISSAC:2023,
    Abstract = {Automating loop analysis, and in particular synthesizing loop invariants, is a central challenge in the computer-aided verification of programs with loops, with applications in compiler optimization, probabilistic programming and IT security. While this challenge is in general undecidable, several techniques have emerged to automatically summarize the functional behaviour of software loops, thus providing inductive loop invariants that may prevent programmers from introducing errors while making changes in their code. In this tutorial, we show that novel combinations of methods from computer algebra, algorithmic combinatorics and static loop analysis provide powerful workhorses to derive (all) polynomial loop invariants, synthesize affine loops from invariants, and infer quantitative properties over the value distributions of probabilistic loop variables.},
    Address = {New York, NY, USA},
    Author = {Kov\'{a}cs, Laura},
    BookTitle = {Proceedings of the 2023 International Symposium on Symbolic and Algebraic Computation},
    File = {Algebra-Based Loop Analysis - 3597066.3597150.pdf},
    ISBN = {9798400700392},
    Keywords = {Loop Synthesis, Loop Invariants, Algebraic Recurrences, Program Verification, Polynomial Ideals},
    Location = {Troms\o{}, Norway},
    Pages = {41--42},
    Publisher = {Association for Computing Machinery},
    Series = {ISSAC '23},
    Title = {Algebra-Based Loop Analysis},
    URL = {https://doi.org/10.1145/3597066.3597150},
    Year = {2023},
    bdsk-url-1 = {https://doi.org/10.1145/3597066.3597150},
    date-added = {2023-08-03 11:23:48 +0200},
    date-modified = {2023-08-03 11:24:05 +0200},
    numpages = {2},
    doi = {10.1145/3597066.3597150}
}

@inproceedings{Kovacs:ISSAC:2023, Abstract = {Automating loop analysis, and in particular synthesizing loop invariants, is a central challenge in the computer-aided verification of programs with loops, with applications in compiler optimization, probabilistic programming and IT security. While this challenge is in general undecidable, several techniques have emerged to automatically summarize the functional behaviour of software loops, thus providing inductive loop invariants that may prevent programmers from introducing errors while making changes in their code. In this tutorial, we show that novel combinations of methods from computer algebra, algorithmic combinatorics and static loop analysis provide powerful workhorses to derive (all) polynomial loop invariants, synthesize affine loops from invariants, and infer quantitative properties over the value distributions of probabilistic loop variables.}, Address = {New York, NY, USA}, Author = {Kov\'{a}cs, Laura}, BookTitle = {Proceedings of the 2023 International Symposium on Symbolic and Algebraic Computation}, File = {Algebra-Based Loop Analysis - 3597066.3597150.pdf}, ISBN = {9798400700392}, Keywords = {Loop Synthesis, Loop Invariants, Algebraic Recurrences, Program Verification, Polynomial Ideals}, Location = {Troms\o{}, Norway}, Pages = {41--42}, Publisher = {Association for Computing Machinery}, Series = {ISSAC '23}, Title = {Algebra-Based Loop Analysis}, URL = {https://doi.org/10.1145/3597066.3597150}, Year = {2023}, bdsk-url-1 = {https://doi.org/10.1145/3597066.3597150}, date-added = {2023-08-03 11:23:48 +0200}, date-modified = {2023-08-03 11:24:05 +0200}, numpages = {2}, doi = {10.1145/3597066.3597150} }