Summarization of branching loops

Abstract:

Handling loops and capturing their semantics represent a significant challenge in software verification; they are one of the causes of the undecidability of this process. In this paper, we present a novel algorithm for the summarization of loops with multiple branches operating over integers. The algorithm is based on analysis of a so-called loop diagram, reflecting the feasibility of various branch interleavings. Summarization can be used to replace loops with equivalent non-iterative statements. This supports the examination of reachability and can be used for software verification. For instance, summarization may also be used for (compiler) optimizations.

BibTeX:

@inproceedings{blicha_summarization_2022,
    title = {{Summarization of branching loops}},
    author = {Blicha, Martin and Kofroň, Jan and Tatarko, William},
    year = {2022},
    booktitle = {{Proceedings of the 37th ACM/SIGAPP Symposium on Applied Computing}},
    publisher = {Association for Computing Machinery},
    series = {{SAC '22}},
    location = {New York, NY, USA},
    doi = {10.1145/3477314.3507042},
    isbn = {978-1-4503-8713-2},
    pages = {1808--1816},
    url = {https://doi.org/10.1145/3477314.3507042},
}

Proceedings paper