Automatic Proof Generation for Linear Arithmetic Prover in Certifying Compiler
Zhang Zhen-ting · Journal of Chinese Computer Systems · 2011
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.