.png){kind=icon}
.png){kind=icon}
Return
CHC-Based Reachability Analysis via Cycle Summarization
.png){kind=icon}
PRE
AI
DOI：10.1007/978-3-032-10794-7_11.png)
.png){kind=icon}
Original request for help.png){kind=icon}
Share.png){kind=icon}
Save
Abstract
En 中文
Modern reachability analysis techniques are highly effective when applied to software safety verification. However, they still struggle with certain classes of problems, particularly the verification of programs with complex control flow and deep nested loops. In this paper, we introduce Cycle Summarization-based Reachability Analysis (CSRA), a new Constrained Horn Clause (CHC) based approach for reachability analysis of nested-loop software. Our technique relies on the generation and refinement of cycle summaries within the CHC system. CSRA analyzes cycles in a modular manner, constructing summaries and cycle unrollings. Cycle summaries in our approach are used both to prove safety and detect potential safety violations. This enables more efficient exploration of nested loops. The prototype of CSRA is implemented within the Golem CHC solver. An empirical comparison with other reachability analysis techniques demonstrates that our approach is highly competitive in both proving safety and constructing counterexamples.
Keywords:
MODEL CHECKING
Journal
I
IF:
0
Papers:
23
Citations:
0