Fundamental Theory Extension And Combinational Logic Verificaition Application Of Theorem Prover Coq

Interactive theorem proving is a main approach, among formal methods, for real sys-tem verification. There have appeared several remarkable achievements recently. How-ever, a often cited drawback of interactive theorem proving is that it is hard to use andit requires a lot of human interaction. The dissertation focuses on Coq, which is oneof the most influential theorem provers. By summarizing the application problems andanalyzingtheunderlyingreasons,thedissertationimprovesCoqintwoaspects. Inthethe-ory side, an extension of fundamental theory of Coq is proposed to improve the equalitychecking ability of Coq. The new extension preserves the properties of the Coq’s theory,thus is able to implement a tool extending Coq. In the application side, a framework forverifying combinational logic is proposed, in which there provides a holistic formalizingand verifying method, as well as an extended library for combinational logic. Verifica-tion of arithmetic units illustrates the ability and features of the framework. The maincontribution of the dissertation is summarized as follows.1. The dissertation extends the Calculus of Inductive Constructions, which is funda-mental theory of Coq, by enriching the intensional equality checking with exten-sional theories. Extensional theory is presented abstractly with requirements. Anytheory satisfying the requirements can be used for extension.2. The extension preserves the properties that are needed for implementing tools. Se-manticpropertiesoftheextensionareprovedinCoq, suchthattheCoqcanorganizecomplex proofs and check the correctness of proofs.3. Presburgerarithmeticisprovedtobeanextensionaltheorysatisfyingalltherequire-ments, which could be used to enrich the equality checking of natural numbers.4. A framework for combinational logic is proposed, which provides a holistic for-malizing and verifying method, as well as an extended library. The good feature ofthe framework makes the verification easier and the result applied more widely.5. Adders are verified as examples to illustrate the usability of the framework. Asystematic verification of adders can also enrich the extended library.