Research On Automatic Specification Generation And Verifica- Tion For Program Verification

With the rapid development of computer science, softwares are becoming increasingly larger and it is becoming increasingly difficult to guarantee the reliability of softwares. Consequently, how to ensure the correctness of softwares is a great challenge in com-puter science. Program verification is able to effectively guarantee the correctness of softwares and improve software reliability. Theorem proving is one of such program verification methods, which works by deductive reasoning to prove the correctness us-ing logics and mathematics. Theorem proving can greatly boost people's confidence in softwares and has become a hot topic. In theorem proving, formal specifications are specified using assertions, based on which verification conditions are generated. Then a theorem proving tool is used to prove the verification conditions. Unfortunately, people are supposed to have a deep understanding of a program to provide suitable specifications and prove these specifications. Such tasks are extremely difficult. And thus automatically generating and verifying specifications is of great importance and significance in program verification. Loop statements are widely used in modern pro-grams and specifications of loops are vital for program verification, especially loop invariants. Unfortunately, loop statements are diverse and complicated, and these is no general way to generate specifications and verify them for all kinds of loops. In addi-tion, modern softwares heavily rely on API libraries. API library behaviors are hence an integral part of software behaviors and specifications of API libraries are funda-mental prerequisites in many program analysis and verification techniques. However, analyzing API libraries to construct specifications is highly challenging due to the lack of source code, implementation in different languages, and complex optimizations. In this thesis, we focus on automatic specification generation for loops and API libraries, and the main contributions are as follows:1. This thesis proposes an approach to automatically infer loop invariants from as-sertions for loops manipulating commonly-used data structures, including nested loops. This approach takes into account of both the program code and program assertions, and it can effectively derive loop invariants to facilitate the code veri-fication. Loop invariant candidates are first generated based on post-conditions of a loop and assertions inside a loop body through simple sub-expression substitution, adding universal quantifier and recurrence relation identification. Then the cor-rectness of each candidate and the relevant assertions are proved using the SMT solver and weakest-precondition calculation. The generated loop invariants can not only describe the shape properties of the iterated data structures, but also specify the relations between elements stored in a data structure, and relations between an element and a scalar variable or a constant. This approach has been implemented and integrated into a code verification tool. The experimental results show that the proposed approach is able to generate dif-ferent kinds of loop invariants, including linear invariants and universally quan-tified invariants, which can greatly facilitate the code verification task.2. This thesis proposes using memories modified by a program statement and new values stored in these memories after executing the statement to summarize the statement. Based on the summary, a loop can be reduced into a sequence of abstract assignments, and a program with loops is transformed into a loop-free program. In this way, we can use techniques that deal with assignments to ana-lyze loops. An approach is presented to automatically synthesize the summary, which can effectively summarize assignments, sequential statements, conditional statement and loops manipulating commonly-used data structures like integer intervals, one-dimensional arrays, two-dimensional arrays and acyclic singly-linked lists. This thesis also proposes a method to generate specifications for program state-ments by analyzing their summaries. The specifications include post-conditions, pre-conditions and loop invariants. We have implemented the proposed approaches. The time used to summarize is in a linear relation to the number of loops. Compared with the methods using abstract interpretation to analyze loops, the proposed approach is much more effi-cient and accurate. The specifications generated through the analysis of the sum-mary of a statement can effectively facilitate the formal verification of programs, which reduce the burden of providing specifications manually, and improve the automatic level and efficiency.3. This thesis proposes a novel approach to generate models from Javadocs in natu-ral languages. These models are code snippets that simulate the functionalities of the original implementations but are much simpler in complexity, which allows software analysis to reason about API library behaviors, without suffering from problems such as lack of source code and complexity in library implementations. This thesis identifies technical challenges of applying natural language process-ing techniques in modeling libraries and proposes solutions that leverage auto testing techniques to solve these problems. We can analyze the models instead of the original complicated source code to generate specifications for API libraries. The models can also replace the original library functions in other software anal-ysis techniques. We have implemented a prototype which automatically models 326 functions in 14 commonly-used Java container classes and 2 Java interfaces. The application of these models in specification generation, Android application static taint anal-ysis and Java dynamic slicing shows that these models precisely represent the API library function behaviors and improve the efficiency and effectiveness of the analysis.