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.