Computer Science ›› 2015, Vol. 42 ›› Issue (12): 47-51.

Previous Articles     Next Articles

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

DONG Yu-chen, WANG Han-fei and ZHAO Jian-hua   

  • Online:2018-11-14 Published:2018-11-14

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

[1] Hoare C A R.An axiomatic basis for computer programming[J].Communications of the ACM,1969,12(10):576-580
[2] D’silva V,Kroening D,Weissenbacher G.A survey of automated techniques for formal software verification[J].IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems,2008,27(7):1165-1178
[3] Aho A V.Compilers:Principles,Techniques and Tools[M].Pearson Education India,2003
[4] Z Jian-hua,L Xuan-dong.Scope Logic:An Extension to Hoare Logic for Pointers and Recursive Data Structures[C]∥Theore-tical Aspects of Computing-ICTAC 2013.Springer Berlin Heidelberg,2013:409-426
[5] De Moura L,Bjrner N.Z3:An efficient SMT solver[M]∥Tools and Algorithms for the Construction and Analysis of Systems.Springer Berlin Heidelberg,2008:337-340
[6] Khedker U,Sanyal A,Sathe B.Data flow analysis:theory and practice[M].CRC Press,2009

No related articles found!
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!