基于数据流分析的单链表可达性自动化验证

Automatic Verification of Singly Linked List Pointer's Reachability Property Using Data-flow Analysis Method

程序验证中的常见情景是判断某个用户指定的性质在程序执行之后或执行过程中的某个程序点上是否成立。人工的形式化验证过程繁琐且容易出错,因此形式化验证的自动化是提高代码验证效率的重要方法。数据流分析技术是一种能够自动发现程序中某类性质的技术。研究了将一种数据流分析技术(单链表形状分析)和基于Scope Logic的代码验证过程相结合的方法。通过数据流分析获得所有程序点上的单链表可达性性质,将结果表达为带有递归函数的一阶逻辑公式,并将其插入到相应程序点中。分析程序还根据Scope Logic的证明法则设定了这些公式之间的逻辑依赖关系。实例测试表明所提方法可以分析得到单链表可达性性质,并且分析结果能够被基于Scope Logic的代码形式化验证过程有效利用,提高了代码形式化证明的效率。

A common scenario in verifying a program is to find out whether some user-specific properties in some program points hold during or after execution. Manual formal verification is tedious and error-prone, so automatic verification is an important way to improve code verification efficiency. Data-flow analysis technique can automatically discover specific properties in programs points. This paper presented a method that integrates a kind of data-flow analysis technique（singly linked list pointers＇ reachability） with Scope-Logic-based code verification. We colleced reachability properties in program points through data flow analysis, presented the results as first order logic formulas with recursive functions, then inserted these formulas into corresponding program points, proved them and established their dependencies according to rules of Scope Logic. Experiments show that our method can acquire singly linked list pointer＇s reachability property efficiently,and the results can be effectively used in code verification in Scope Logic.