Dissertation > Excellent graduate degree dissertation topics show
Proof Generation for Certifying Compiler
Author: YangSiMin
Tutor: ChenYiYun
School: University of Science and Technology of China
Course: Computer Software and Theory
Keywords: Prove generate Automated Theorem Proving Integer linear theorem proving Certifying compiler Program Verification High Confidence Software
CLC: TP314
Type: Master's thesis
Year: 2010
Downloads: 40
Quote: 1
Read: Download Dissertation
Abstract
With the rapid development of computer science and technology, increasingly largescale computer software, and more and more difficult to debug and maintain. On the other hand, software security situation is grim, untrusted source code security implementation issues gradually emerged. In this context, the relationship between the key areas of the national economy and the industry, the increasing demand for high trusted software. Formal procedures to verify the nature of the formal procedures in the various build high trusted software technology, and give a formal proof to guarantee the security of the software can theoretically guarantee program run without violation of safety norms. Certifying compiler as an important branch of verifying compiler, a combination of modern compiler technology and program verification methods the source annotation generates the corresponding proof of the nature of the proceeding in the assembly code is generated at the same time, according to the programmer. Code consumer side only need to use a trusted proof checker to statically check the generated proof, check the security of the program can be indirectly compiler to exclude the Trusted Computing Base. In the theoretical framework for certifying compiler, technology plays a key role in automated theorem proving. Does not support automatic theorem proving, proof of the nature of the proceeding all require programmers to manually enormous workload. Issued early in the laboratory on the basis of the proof of the compiler project PLCC, a certifying compiler CComp, and its main features is to use Hoarestyle program verification methods have been designed and implemented, the application of separation logic express verification conditions, in particular with regard to pointer verification conditions, while the introduction of a modern automatic theorem proving automatic proof verification conditions, learn the formal definition based the stack verify assembler programming framework to build the backend of the target program verification framework. Embedded automated theorem proving, the main support for the integer linear theory and separation logic, and can generate by the auxiliary theorem proving tools Coq check the prove. In this paper, we first introduce the background and current status of the project, and then briefly the certifying compiler design CComp, including the source language, the assertion language, sourcelevel verification framework and targetlevel verification framework. Sourcelevel verification framework, this paper focuses on the design and implementation of the Simplex algorithm and Boundand Branchbased approach integer linear theorem proving, and I put forward for the conservation, management prove proof library for information and generate proof mechanism described some key algorithm, truthfully number satisfiability checking process, prove the preservation process that information in the library, to prove the main algorithm generated. Finally, this paper gives two simple tests. The results show that the integer linear theorem prover can automatically prove certifying compiler validation conditions CComp generated integer linear program, and its proven superior Coq proving strategy Omega generate proof generated. The main contribution of this paper is as follows: 1. Based on the Simplex algorithm and Bound and Branch method, designed and implemented a support Proposition solving linear integer automatic theorem prover for proof of verification conditions CComp in linear integer. 2 presented its own set of proof items constructed for automatic theorem prover Coq. Inspection certificate is generated. This method can be automatically configured proof items need to select the already fragmented prove information, and combine them to form a substantially free of redundancy proof items. The proof items generate proof items with Coq comes proof strategy to generate even more than simple. The significance of this work is to check proof generation exploration the linear integer theorem proving machine, put forward a new method used to construct the proof items accumulated technical aspects of domainspecific logic automated theorem proving research experience laid the theoretical and technical foundation for the future to achieve automatic program verification, Building High Confidence Software.

Related Dissertations
 Application and Research of Finite Element Method Among Lue Yang Electric Factory Slope Stability Analysis,TU43
 The Study on Network Planning and Optimization Technology of IP Core Networks,TN915.02
 A Method to Generate Assertion and Proof about Assembly Language Certifying Compiler,TP314
 The Proof Methods of Constructive and Nonconstructive Geometric Theorems,O18
 The Analysis of Isabelle Theorem Prover and Its Application in PAR Method/PAR Platform,TP311.11
 Verify with dynamic thread creation and exit multithreaded programs,TP311.53
 Analysis and Testing of Web Services Choreography Description Language,TP393.09
 A program verification tool design and implementation,TP311.53
 The Function Differential, Partial Differentiation, Grads, Divergence, and Curl in Mizar,TP399C5
 Axiomatic Semantics of Class and Polymorphism for Java,TP312
 The Study and Development of the Simulation Programmer for NC Lathers,TG519.1
 Design and Implementation of Static Verifier in VeriJava,TP312.1
 Research on Automatic Theorem Proving Based on Grid Computation,TP393.01
 Axiomatic semantics of the Java language 's exception handling mechanism,TP312
 Research on Methods of Security Assurance Based on ComputerAssisted Proof,TP309
 Study on Program Verification,TP311.11
 Verification of Lowlevel Concurrent Code with Several Synchronization Mechanisms,TP332
 Research on Visually Dynamic Presentation of Proofs in Plane Geometry,TP391.41
 Automated Loop Invariant Generation for Program Verification,TP311.11
 Verifying Parallel Programs Using Software Transactional Memory,TP311.5
CLC: > Industrial Technology > Automation technology,computer technology > Computing technology,computer technology > Computer software > Compiler,interpreter
© 2012 www.DissertationTopic.Net Mobile
