Proceedings paper

Title:
Summarization of Branching Loops
Authors:
M. Blicha, J. Kofroň, W. Tatarko
Publication:
Proceedings of The 37th ACM/SIGAPP Symposium on Applied Computing (SAC '22)
DOI:
Year:
2022
ISBN:
978-1-4503-8713-2

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 (SAC '22)}},
    publisher = {ACM Press},
    location = {Virtual event},
    doi = {10.1145/3477314.3507042},
    isbn = {978-1-4503-8713-2},
    pages = {9},
}