.png){kind=icon}
返回
Termination Resilience Static Analysis
.png){kind=icon}
PRE
AI
DOI：10.1007/978-3-032-15700-3_11.png)
.png){kind=icon}
原文求助.png){kind=icon}
分享.png){kind=icon}
收藏
摘要
En 中文
我们提出了一种基于抽象解释的静态分析框架，用于证明终止鲁棒性，即软件系统中不存在鲁棒非终止漏洞。鲁棒非终止表征了那些不受信任（如外部控制）的输入可以强制无限执行，而与其它受信任（如受控）变量无关的程序。我们的框架是Cousot和Cousot基于抽象解释的排序函数推导的语义泛化，我们的健全静态分析以非平凡的方式扩展了Urban和Mine的决策树抽象域，以区分不受信任和受信任的程序变量。我们的方法已实现在一个开源工具中，并在来自SV-COMP且基于真实软件的基准上进行了评估，展示了在验证终止鲁棒性和检测潜在鲁棒非终止漏洞方面的实际有效性。
Keyword:
Termination Resilience
Abstract Interpretation
Static Analysis
Robust Non-Termination
Ranking Function
期刊
V
机构
引用论文
分享收藏An abstract interpretation framework for termination终止性的一种抽象解释框架.png)
Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages
Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languagesIF0
PREAI
分享收藏
查看更多内容