Reachability Analysis for Multiloop Programs Using Transition Power Abstraction

Abstract:

A wide variety of algorithms is employed for the reachability analysis of programs with loops but most of them are restricted to single loop programs. Recently a new technique called Transition Power Abstraction (TPA) showed promising results for safety checks of software. In contrast to many other techniques TPA efficiently handles loops with a large number of iterations. This paper introduces an algorithm that enables the effective use of TPA for analysis of multiloop programs. The TPA-enabled loop analysis reduces the dependency on the number of possible iterations. Our approach analyses loops in a modular manner and both computes and uses transition invariants incrementally, making program analysis efficient. The new algorithm is implemented in the Golem solver. Conducted experiments demonstrate that this approach outperforms the previous implementation of TPA and other competing tools on a wide range of multiloop benchmarks.

BibTeX:

@inproceedings{britikov_reachability_2024,
    title = {{Reachability Analysis for Multiloop Programs Using Transition Power Abstraction}},
    author = {Britikov, Konstantin and Blicha, Martin and Sharygina, Natasha and Fedyukovich, Grigory},
    year = {2024},
    booktitle = {{Formal Methods}},
    editor = {Platzer, André and Rozier, Kristin Yvonne and Pradella, Matteo and Rossi, Matteo},
    publisher = {Springer Nature Switzerland},
    location = {Cham},
    doi = {10.1007/978-3-031-71162-6_29},
    isbn = {978-3-031-71162-6},
    pages = {558--576},
}

Proceedings paper