Practical Tactics For Verifying C Programs In Coq

The computer system has been widely used in the key areas of national defense, communication, finance, energy, transportation, medical treatment, etc. Building high confident system software has become an important topic in the world. The safety and reliability of the operating system kernel is extremely important to building high confident computer system, because any tiny kernel errors are likely to lead to the crush of the entire computer system. Formal program verification is an approach to guarantee the correctness of computer programs with logical reasoning system. It is one of the most effective approaches to ensure safety and reliability of system kernel whose design is complex but with relatively small scale.Most low-level system software is implemented with C programming language. The large number of pointer operations and the complicate logical relations among the involved data structures require that the assertion language used for specifying system software should be expressive enough. However, the fully automated verification pro-cedures cannot be achieved with the expressive assertion language because their logic reasoning system are always undecidable. In fact, the existing projects on system soft-ware verification have shown that manual verification of system software requires a lot of manpower and material resources in theorem proving tools. Therefore, how to improve the efficiency of the verification of C program as much as possible without sacrificing the expressiveness of logic assertions is an urgent problem to be solved.In this thesis, we have improved the efficiency of the verification of C program in the theorem prover Coq by developing practical tactics. Considering man-machine interactive proof of a complex operating system is inevitable, therefore, in the process of developing automatic tactics, we must take the following two aspects into account: on the one hand, the tactics should reduce manual proofs as much as possible, and on the other hand, the tactics should provide user-friendly and useful error messages when the automated verification fails, so that users could easily locate where the problem is. Users may adjust specifications or the code accordingly, or to do part of the proofs manually. Based on the above considerations, we have developed a set of practical tac-tics for verifying C programs in Coq, including both tactics for automatically proving separation logic assertions and ones for automatically generating and proving the verifi-cation condition of a Hoare triple. These tactics have taken both efficiency and usability into account.This thesis makes the following contributions:· We incorporate domain-specific knowledge on data structures (like singly-linked lists) in the verification process and automatically unfold the appropriate induc-tive predicates to improve the efficiency of verifying C programs.· We introduce a resource check procedure (just like a pre-processing) in our tac-tics to give users the related error message, which could help them locate where the bug is. It greatly improves the usability when man-machine interaction is necessary.· Based on the two ideas above, we have implemented a set of practical tactics (about10,000lines of Coq codes) for verifying C programs in Coq. With these tactics we are able to verify some simple list manipulating C programs fully au-tomatically.