.png){kind=icon}
.png){kind=icon}
Return
Termination Resilience Static Analysis
.png){kind=icon}
PRE
AI
DOI：10.1007/978-3-032-15700-3_11.png)
.png){kind=icon}
Original request for help.png){kind=icon}
Share.png){kind=icon}
Save
Abstract
En 中文
We present a novel abstract interpretation-based static analysis framework for proving Termination Resilience, the absence of Robust Non-Termination vulnerabilities in software systems. Robust Non-Termination characterizes programs where an untrusted (e.g., externally-controlled) input can force infinite execution, independently of other trusted (e.g., controlled) variables.Our framework is a semantic generalization of Cousot and Cousot's abstract interpretation-based ranking function derivation, and our sound static analysis extends Urban and Mine's decision tree abstract domain in a non-trivial way to manage the distinction between untrusted and trusted program variables. Our approach is implemented in an open-source tool and evaluated on benchmarks sourced from SV-COMP and modeled after real-world software, demonstrating practical effectiveness in verifying Termination Resilience and detecting potential Robust Non-Termination vulnerabilities.
Keywords:
Termination Resilience
Abstract Interpretation
Static Analysis
Robust Non-Termination
Ranking Function
Journal
V
IF:
0
Papers:
18
Citations:
0