| 出具证明编译器中线性整数命题证明的自动生成 |
| |
| 引用本文： | 杨思敏,李兆鹏,庄重,张臻婷.出具证明编译器中线性整数命题证明的自动生成[J].小型微型计算机系统,2011,32(6). |
| |
| 作者姓名： | 杨思敏 李兆鹏 庄重 张臻婷 |
| |
| 作者单位： | 中国科学技术大学计算机科学与技术学院,合肥,230026;中国科学技术大学苏州研究院,江苏苏州,215123 |
| |
| 基金项目： | 国家自然科学基金项目(90718026,60928004)资助 |
| |
| 摘 要： | 近年来,出具证明编译器作为构建高可信软件的重要途径,逐渐成为编译器理论和形式化验证的研究热点.在其理论框架中,编译器需要借助自动定理证明技术,自动地证明验证条件并生成机器可检查的证明项,因此好的自动定理证明器对出具证明编译器至关重要.本文基于Simplex算法在出具证明编译器的框架内设计并实现了一个支持线性整数命题求解的自动定理证明器,并且提出一套证明项构造方法,将其应用于自动定理证明器中可生成Coq可检查的证明.
|
| 关 键 词： | 证明生成 自动定理证明 整数定理证明 出具证明编译器 |
Automatic Proof Generation for Linear Arithmetic Prover in Certifying Compiler |
| |
| YANG Si-min,LI Zhao-peng,ZHUANG Zhong,ZHANG Zhen-ting.Automatic Proof Generation for Linear Arithmetic Prover in Certifying Compiler[J].Mini-micro Systems,2011,32(6). |
| |
| Authors: | YANG Si-min LI Zhao-peng ZHUANG Zhong ZHANG Zhen-ting |
| |
| Affiliation: | YANG Si-min1,2,LI Zhao-peng1,ZHUANG Zhong1,ZHANG Zhen-ting1,2 1(School of Computer Science and Technology,University of Science and Technology of China,Hefei 230026,China) 2(Suzhou Institute for Advanced Study,Suzhou 215123,China) |
| |
| Abstract: | 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 g... |
| |
| Keywords: | proof generation automated theorem proving linear arithmetic proving certifying compiler |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
|
