Sciweavers

Share
TASE
2007
IEEE

Design of a Certifying Compiler Supporting Proof of Program Safety

9 years 2 months ago
Design of a Certifying Compiler Supporting Proof of Program Safety
Safety is an important property of high-assurance software, and one of the hot research topics on it is the verification method for software to meet its safety policies. In our previous work, we designed a pointer logic system and proposed a framework for developing and verifying safetycritical programs. And in this paper, we present the design and implementation of a certifying compiler based on that framework. Here we will mainly explain verification condition generation, generation of code and assertions, and proof generation for basic blocks. Our certifying compiler has the following novelties: 1) it supports a programming language equipped with both a type system and a logic system; 2) and it can produce safety proofs for programs with pointers.
Yiyun Chen, Lin Ge, Baojian Hua, Zhaopeng Li, Chen
Added 04 Jun 2010
Updated 04 Jun 2010
Type Conference
Year 2007
Where TASE
Authors Yiyun Chen, Lin Ge, Baojian Hua, Zhaopeng Li, Cheng Liu
Comments (0)
books