An Automatic Program Verification Tool For Pointerc: Design And Implemetation

With the continuous development of computer technology, the country, society and everyday life shows a growing dependence on software systems, as well with an increasing demand for high-confidence software. Formal verification is a major method to improve the dependability of the software. One of the hot research areas is automatic program verification based on logical inference, but verification of programs property dealing with pointers remain difficult problems so far. Since Hoare logic is unable to handle the programs with aliases, previous studies use complicated extended Hoare logic to solve the aliasing programs, such as separation logic, with generated verification too complex to prove automatically.Based on these previous studies in the field of program verification, we propose a new way to solve the aliasing problem of pointer programs in program verification, design and implement a source-level program verification tool, which main feature is to support program verification using information provided with shape system, on the basis of program point shape graph through program analysis. This paper proposes a method using regular Hoare logic rules to reason about assignment not dealing with pointers in a C-like programming language, such rules will be applied before aliasing is eliminated using information of shape graphs. At the same time, we introduces modern automated theorem proving technology to automatically prove the verification conditions, especially an approach to verify data constrains on mutable data structures without using user-defined predicates. The author take charge of the design and implementation of the program verification tool for PointerC language with the above-mentioned methods. This verification tool automatically verifies not only the property of programs dealing with mutable data structure, but also programs dealing with one-dimension arrays and simple types.The main contributions of the thesis are:1. Designed a method of using the shape graphs information to eliminate the aliasing problem, enabling to use Hoare logic to verify the pointer programs, and gave a summary prove about the soundness of the method.2. Designed a method of verify data constrains on mutable data structures without using user-defined predicates.3. Designed and implemented a program verification tool for PointerC language, which can automatically verify programs manipulating recursive data structures and programs dealing with one-dimension arrays and simples types.The significance of this work lies in a new approach to figure out the difficulties in analysis and verification of pointer programs, and the implementation of a program verification tool. This work accumulated the experience in the field of program verification, and laid the theoretical and technical basis for automatic program verification and building high-confidence software in the future.