Slicing Execution For Verification Of C Programs

With the wide using of computer systems, the trustworthy properties of the software are receiving more and more attentions. The formal verification of the software program is one of the effective methods to promise trustworthy. Therefore, more and more researchers are attracted to this area. However, the software programs usuallyhave complex logic and large scale, so how to increase the accuracy and the scalability of the program verification is the main research topic.The dissertation presents a novel method, namely slicing execution, to verify C programs with respect to temporal safety properties. It is basically a lightweight symbolic execution technical, and may automatically extract finite models from sequential and concurrent C programs. Slicing execution integrates several state space reduction techniques, including program slicing, abstraction of program semantics, symbolical representation, counterexample guided abstraction refinement andpartial-order reduction, etc. Therefore, the state spaces of the abstracted models can begreatly reduced, and the scalability of the verification can be improved correspondingly. The distinguished feature of slicing execution is that it may achieve the accuracy of path-sensitive simulation for verifying temporal safety properties, only with the cost close to standard flow-sensitive dataflow analysis. More than that, it supports arbitrary program structure including all kinds of program loops. It can also full-automatically abstract models and verify properties without any aid of people.Slicing execution is founded on the over-approximated program semantics of C programs by variable abstraction. It only symbolically executes the relevant statements under variable abstraction, and calculates the partial strongest post-conditions and the partial weakest preconditions to construct finite abstract models, which may be model checked with respect to temporal safety properties. Based on the verification reusing framework presented in the dissertation, slicing execution keeps refining the variable abstraction criteria according to the spurious counterexample paths until the property is proven or a feasible counterexample path is found. To verify concurrent C programs, a novel stateful dynamic partial-order reduction method is integrated into slicing execution, which greatly reduces the searching state space. A lightweight decision procedure is also integrated to efficiently decide the formulas generated during the verification of C programs. More thoroughly, the innovations of the dissertation are summarized into following five aspects: 1. The basic definitions and techniques for slicing execution. Based on the analysis of practical program verification, we present variable abstraction to only consider the variables and statements that are relevant to the given property. We then present the partial strongest post-condition, which represents the over-approximated program semantics. Finally, we present slicing execution as a lightweight symbolic execution.2. The temporal safety property oriented searching reusing framework and its application in slicing execution. Like counterexample guided abstraction refinement (CEGAR), the searching reusing framework also refines the abstracted model under the guidance of spurious counterexamples. However, it makes the searching information be reused among the models of different precision, and thus a great deal of redundant searching may be avoided.3. The definition of partial weakest precondition and its application in slicing execution. The partial weakest precondition is another way to represent the over-approximated program semantics, and its definition is also based on variable abstraction. In slicing execution, we may use partial weakest preconditions to replace part of partial strongest post-conditions to generate much weaker state formulas. As a result, we may greatly reduce the state space of the abstracted model without loss of accuracy.4. The stateful dynamic partial-order reduction technique and its application in slicing execution. After extending slicing execution to concurrent C programs, we present the stateful dynamic partial-order reduction technique to guide it not to search multiple interleaving transition sequences that has the same partial-order. We select several experiments including two practical program fragments and a concurrent SSL system. The experiments illustrate that the integration of slicing execution and stateful dynamic partial-order reduction leads to the reduction of the state space, as well as the reduction of the space cost of the verification.5. The lightweight decision procedure for the verification formulas of slicing execution. We define an extended class of integer linear first-order logic formula, which supports most integer linear and bit-wise expressions in C programs including integer division, integer modular and bit-wise operation. Experiment results show that the extended decision procedure supports most verification formulas met in slicing execution. Based on the experiment over the practical program openssl-0.9.6c, we find that the decision cost is 10.5 times less than the theorem prover Simplify.Our slicing execution tool prototype is implemented on the open-source project MAGIC. Each innovation is demonstrated by an experiment on the practical program openssl-0.9.6c. We also compare our experiment results with BLAST and MAGIC. All experiments are performed on machines of same hardware, using same practical program and verifying same properties. The comparing results show that slicing execution is even a bit more effective than the other two.