Generation of Violation Witnesses by Under-Approximating Abstract Interpretation
VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION, VMCAI 2024, PT I(2024)
摘要
This works studies abstract backward semantics to infer sufficient program preconditions, based on an idea first proposed in previous work [38]. This analysis exploits under-approximated domain operators, demonstrated in [38] for the polyhedra domain, to under-approximate Dijkstra's liberal precondition. The results of the analysis were implemented into a static analysis tool for a toy language. In this paper we address some limitations that hinder its applicability to C-like programs. In particular, we focus on two improvements: handling of user input and integer wrapping. For this, we extend the semantic and design sound and effective abstractions. Furthermore, to improve the precision, we explore an under-approximated version of the power-set construction. This in particular helps handling arbitrary union that is difficult to implement with under-approximated domains. The improved analysis is implemented and its performance is compared with other static analysis tools in SV-COMP23 using a selected subset of benchmarks.
更多查看译文
关键词
Abstract interpretation,Software verification,Program analysis,Bug catching,Under-approximation
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要