A Unifying Approach for Control-Flow-Based Loop Abstraction

Beyer, Dirk ; Lingsch Rosenfeld, Marian und Spiessl, Martin (2022): A Unifying Approach for Control-Flow-Based Loop Abstraction. 20th International Conference on Software Engineering and Formal Methods, SEFM 2022, Berlin, Germany, September 26–30, 2022. Schlingloff, Bernd-Holger und Chai, Ming (Hrsg.): In: Software Engineering and Formal Methods. 20th International Conference, SEFM 2022, Berlin, Germany, September 26–30, 2022, Proceedings, Lecture Notes in Computer Science Bd. 13550 Cham, Switzerland: Springer. S. 3-19

Abstract

Loop abstraction is a central technique for program analysis, because loops can cause large state-space representations if they are unfolded. In many cases, simple tricks can accelerate the program analysis significantly. There are several successful techniques for loop abstraction, but they are hard-wired into different tools and therefore difficult to compare and experiment with. We present a framework that allows us to implement different loop abstractions in one common environment, where each technique can be freely switched on and off on-the-fly during the analysis. We treat loops as part of the abstract model of the program, and use counterexample-guided abstraction refinement to increase the precision of the analysis by dynamically activating particular techniques for loop abstraction. The framework is independent from the underlying abstract domain of the program analysis, and can therefore be used for several different program analyses. Furthermore, our framework offers a sound transformation of the input program to a modified, more abstract output program, which is unsafe if the input program is unsafe. This allows loop abstraction to be used by other verifiers and our improvements are not ‘locked in’ to our verifier. We implemented several existing approaches and evaluate their effects on the program analysis.

• Dokumententyp: Konferenzbeitrag (Paper)
• Fakultät: Mathematik, Informatik und Statistik > Informatik
• Themengebiete: 000 Informatik, Informationswissenschaft, allgemeine Werke > 004 Informatik
• ISSN: 0302-9743
• Ort: Cham, Switzerland
• Sprache: Englisch