loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering (TASE '07)
Design of a Certifying Compiler Supporting Proof of Program Safety
Shanghai, China
June 06-June 08
ISBN: 0-7695-2856-2
ASCII Text
x 
 
Yiyun Chen, Lin Ge, Baojian Hua, Zhaopeng Li, Cheng Liu, "Design of a Certifying Compiler Supporting Proof of Program Safety," Theoretical Aspects of Software Engineering, Joint IEEE/IFIP Symposium on, pp. 127-138, First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering (TASE '07), 2007.
 
 
BibTex
x
 
@article{ 10.1109/TASE.2007.19,
author = {Yiyun Chen and Lin Ge and Baojian Hua and Zhaopeng Li and Cheng Liu},
title = {Design of a Certifying Compiler Supporting Proof of Program Safety},
journal ={Theoretical Aspects of Software Engineering, Joint IEEE/IFIP Symposium on},
volume = {0},
year = {2007},
isbn = {0-7695-2856-2},
pages = {127-138},
doi = {http://doi.ieeecomputersociety.org/10.1109/TASE.2007.19},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - Theoretical Aspects of Software Engineering, Joint IEEE/IFIP Symposium on
TI - Design of a Certifying Compiler Supporting Proof of Program Safety
SN - 0-7695-2856-2
SP127
EP138
A1 - Yiyun Chen,
A1 - Lin Ge,
A1 - Baojian Hua,
A1 - Zhaopeng Li,
A1 - Cheng Liu,
PY - 2007
KW - null
VL - 0
JA - Theoretical Aspects of Software Engineering, Joint IEEE/IFIP Symposium on
ER -
 
Yiyun Chen, University of Science and Technology of China
Lin Ge, University of Science and Technology of China
Baojian Hua, University of Science and Technology of China
Zhaopeng Li, University of Science and Technology of China
Cheng Liu, University of Science and Technology of China
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.
Citation:
Yiyun Chen, Lin Ge, Baojian Hua, Zhaopeng Li, Cheng Liu, "Design of a Certifying Compiler Supporting Proof of Program Safety," tase, pp.127-138, First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering (TASE '07), 2007
Usage of this product signifies your acceptance of the Terms of Use.