Finding Inconsistencies in Programs with Loops.
LPAR(2015)
摘要
Inconsistent code is an important class of program abnormalities that appears in real-world code bases and often reveals serious bugs. A piece of code is inconsistent if it is not part of any safely terminating execution. Existing approaches to inconsistent code detection scale to programs with millions of lines of code, and have lead to patches in applications like the web-server Tomcat or the Linux kernel. However, the ability of existing tools to detect inconsistencies is limited by gross over-approximation of looping control-flow. We present a novel approach to inconsistent code detection that can reason about programs with loops without compromising precision. To that end, by leveraging recent advances in software model checking and Horn clause solving, we demonstrate how to encode the problem as a sequence of Horn clauses queries enabling us to detect inconsistencies that were previously unattainable.
更多查看译文
关键词
Inconsistent Coding, Software Model Checking, Constrained Horn Clauses (CHCs), Blocking Clause, Feasible Execution
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络