Dissertation > Excellent graduate degree dissertation topics show

Slicing Execution for Verification of C Programs

Author: YiXiaoDong
Tutor: YangXueJun;WangZuo
School: National University of Defense Science and Technology
Course: Computer Science and Technology
Keywords: slicing execution model checking temporal safety property C program verification variable abstraction partial strongest post-condition partial weakest precondition stateful dynamic partial-order reduction
CLC: TP312.1
Type: PhD thesis
Year: 2006
Downloads: 408
Quote: 3
Read: Download Dissertation


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.

Related Dissertations

  1. Research on the Methods for Detecting Mismatch of Web Services Based on Bounded Model Checking,TP311.52
  2. Research on a Secure E-Commerce Payment Protocol Based on Four Parties,TP393.08
  3. Application and Research of Finite Element Method Among Lue Yang Electric Factory Slope Stability Analysis,TU43
  4. Research on UML Modeling and Model Checking of CTCS-3 Train Control System,TP273
  5. Design and Implementation Automatic Analyzer for Security Protocol,TP393.08
  6. Formal Analysis and Verification of a Transaction Coordination Protocol Named WS-TX for Web Services,TP393.09
  7. Research on Security of E-Commerce Protocols Based on UPPAAL,TP393.08
  8. Timed automata model - based verification techniques,TP301.1
  9. Forecasting Model and Applied Research of Based on Time Series ARCH,O211.61
  10. Studies on the Dynamic Simulation Models for Growth of Super Hybrid Rice Seedings,S511
  11. The Monitoring of Farmland Soil Moisture and Water Management System for Cotton on Drip Irrigation under Mulch,S562
  12. Research on Model Checking Algorithms of Ambients Calculi Systems,TP274
  13. The Analysis of Model Checking and Verification System of Network Security Protocol,TP393.08
  14. Research and Implement on Static Malware Detection System Based on Program Semantics,TP393.08
  15. The Application and Implemenation of PPTL Model Checking Tool,TP311.52
  16. Simulation and Analysis of Schedule Strategy of Reconfigrable HW System,TN791
  17. The Study on Network Planning and Optimization Technology of IP Core Networks,TN915.02
  18. Research on Interaction Adaptation of Time-Aware Web Services,TP393.09
  19. Research on Verification of Web Service Composition Based on XYZ/ADL,TP393.09
  20. Proof Generation for Certifying Compiler,TP314
  21. A Method to Generate Assertion and Proof about Assembly Language Certifying Compiler,TP314

CLC: > Industrial Technology > Automation technology,computer technology > Computing technology,computer technology > Computer software > Programming language ALGOL
© 2012 www.DissertationTopic.Net  Mobile