出具证明编译器中线性整数命题证明的自动生成  

Automatic Proof Generation for Linear Arithmetic Prover in Certifying Compiler

作　　者：杨思敏[1,2] 李兆鹏[1,2] 庄重[1,2] 张臻婷[1,2] 

机构地区：[1]中国科学技术大学计算机科学与技术学院,合肥230026 [2]中国科学技术大学苏州研究院,江苏苏州215123

出　　处：《小型微型计算机系统》2011年第6期1175-1180,共6页Journal of Chinese Computer Systems

基　　金：国家自然科学基金项目(90718026;60928004)资助

摘　　要：近年来,出具证明编译器作为构建高可信软件的重要途径,逐渐成为编译器理论和形式化验证的研究热点.在其理论框架中,编译器需要借助自动定理证明技术,自动地证明验证条件并生成机器可检查的证明项,因此好的自动定理证明器对出具证明编译器至关重要.本文基于Simplex算法在出具证明编译器的框架内设计并实现了一个支持线性整数命题求解的自动定理证明器,并且提出一套证明项构造方法,将其应用于自动定理证明器中可生成Coq可检查的证明.Recently,as an important way to build high-confidence software,certifying compiler is becoming the research focus of the compiler and formal verification.In its theoretical framework,the compiler proves the verification conditions and generates the machine-checkable proof automatically with automated theorem prover,so a good automated theorem prover is essential for certifying compiler.This paper describes a linear arithmetic prover based on the Simplex algorithm,and proposes an innovative method of proof generation,which is applied to our automated theorem prover to build the Coq-checkable proof.

关 键 词：证明生成 自动定理证明 整数定理证明 出具证明编译器 

分 类 号：TP313[自动化与计算机技术—计算机软件与理论]