关键词: 代码验证,数据流分析,Scope Logic

Abstract: 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 pro-perties 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.

Key words: Code verification,Data-flow analysis,Scope Logic