The Implementation Of Expansion For Shape Graph Logic

The development of the information age leads software applications to every family and all works of life. With the rapid expansion of the range and scale of software applications, the requirement for software security is improving. The increasing of the cost for software testing and maintenance made the software security more important. The formal verification based on logical inference is an important method to improve the software reliability. In the21th century, people all over the world have done a lot of research and development on the spread and industry application of this method. Our lab (USTC-Yale Joint Research Center for High-Confidence Software) is active in research for verification methods of parallel programming and verification tools of serial programming.This work is the extension of an automatic program verification prototype system for PointerC. It is mainly a test tool on the verification of pointer programs.This paper proposes a series of inference rules for assignment statement of One-Dimensional array elements. And it designs and implements a formal verification method for programs on data structures with additional list.The main contributions of this paper are as follows:Firstly, this paper proposes a series of inference rules for assignment statement of array elements, and extends it to be used in verification of progams with universal quantifier assertions containing superscript expressions.The prototype system is mainly designed for pointer program. But in the meantime, it is for verifications of program with other kinds of structures like array programs. In programs operating on one-dimensional array, quantified assertions (like universal quantifier assertions) are needed to express properties of arrays. Once we need to use the assignment axiom on deducing assignment statement, this inference rules must be used to help. The same way, this inference rules is applicable in verification of progams with universal quantifier assertions containing superscript expressions.Secondly, we design and implement a formal verification method for programs on data structures with additional list.During the shape analysis of the pointer program, pointing the additional list pointers to the primary shape nodes, would lead to the impossibility of accurate pointer analysis. Furthermore, the shape graph logic based on accurate pointer analysis would also be useless. The solusion in this paper is to separate the additional list from the primary shape graph to build a virtual additional list.Through the implementation the above improvement of expansion for shape graph logic, the prototype system is extended to verify some complex one dimensional array programs and progams with universal quantifier assertions containing superscript expressions.