Publications

[home]

2011

  1. A Generator for Verification Condition Generator. Zhaopeng Li, Yang Zhang, Yiyun Chen. Accepted by the 5th IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE'11), August, Xi’an, China
  2. Automatic Proof Generation for Linear Arithmetic Prover in Certifying Compiler. Simin Yang, Zhaopeng Li, Zhong Zhuang, and Zhenting Zhang. Accepted by Journal of Chinese Computer Systems,2010. (In Chinese) (pdf)
  3. Assertion and Proof Generation for Assembly Code in Certifying Compiler. Zhenting Zhang, Zhaopeng Li, Yiyun Chen, Simin Yang, and Zhong Zhuang. Accepted by Journal of Chinese Computer Systems,2010. (In Chinese) (pdf)
  4. Code Optimization and Specification Transformation in Certifying Compiler. Dawei Fan, Zhaopeng Li, and Xinyu Jiang. Accepted by Journal of Chinese Computer Systems,2010. (In Chinese) (pdf)

 

2010

  1. A Pointer Logic Dealing with Uncertain Equality of Pointers. Hongjin Liang, Yu Zhang, Yiyun Chen, Zhaopeng Li, and Baojian Hua. Chinese Journal of Software, 2010, Vol.21(No.2):334-343.(In Chinese) (pdf)
  2. A Pointer Logic for Verification of Pointer Programs. Yiyun Chen, Zhaopeng Li, Zhifang Wang, and Baojian Hua. Chinese Journal of Software,2010, Vol.21(No.3):415-426. (In Chinese) (pdf)
  3. A Certifying Compiler for Clike Subset of C Language. Zhaopeng Li, Zhong Zhuang, Yiyun Chen, Simin Yang, Zhenting Zhang and Dawei Fan. Accepted by the 4th IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE'10), August 25 - 27, 2010, Taipei, Taiwan, China (pdf)

2009

  1. A Pointer Logic for Verification of Pointer Programs. Yiyun Chen, Zhaopeng Li, Zhifang Wang, Baojian Hua. In the INFORMAL proceeding of 6th Sixth Asian Workshop on Foundations of Software(AWFS2009), Tokyo, Japan, April 6-8, 2009. (pdf)
  2. An Assembly Pointer Logic: Design and Implementation.  Zhaopeng Li, Yiyun Chen, Baojian Hua, Wang Wei, Tian Bo. Journal of  Chinese Computer Systems, 30(6):1025-1030, June 2009. (In Chinese) (pdf)
  3. Design and Implementation of a Back-end for a Certifying Compiler.Bo Tian, Yiyun Chen, Wei Wang, Zhaopeng Li, Zhifang Wang. Chinese Journal of Computer Engineering and Applications. 35(7):132-135, April 2009.

2008

  1. Certifying the Safety of Assembly Pointer Programs. Zhaopeng Li. Ph.D. dissertation, Department of Computer Science and Technology, University of Science & Technology of China, July 2008.(pdf)
  2. Automatic Generation of Formal Specifications in Assembly Code Certification. Lin Ge, Yiyun Chen, Baojian Hua, Zhaopeng Li, Cheng Liu.  Journal of  Chinese Computer Systems, 29(7):1219-1224, July 2008.
  3. A Certified Type Checker for Typed Assembly Language. Yu Guo, Yiyun Chen, Baojian Hua, Zhaopeng Li. Journal of  Chinese Computer Systems, 29(7):1230-1236, July 2008.
  4. A Formal Certifying Framework For Assembly Programs. Zhaopeng Li, Yiyun Chen, Lin Ge, and Baojian Hua. Chinese Journal of Computer Research and Development, 45(5):825-833, May 2008. [ bib | .pdf ]
  5. Design and Proof of a Safe Programming Language PointerC. Baojian Hua, Yiyun Chen, Zhaopeng Li, Zhifang Wang, and Lin Ge.  Chinese Journal of Computers, 31(4):556-564, April 2008. [ bib | .pdf ]

2007

  1. A Pointer Logic and Certifying Compiler. Yiyun Chen, Lin Ge, Baojian Hua, Zhaopeng Li, Cheng Liu, and Zhifang Wang.  Frontiers of Computer Science in China, 1(3):297-312, Jul 2007. [ bib | .pdf ]
  2. Design of a Certifying Compiler Supporting Proof of Program Safety. Yiyun Chen, Lin Ge, Baojian Hua, Zhaopeng Li, Cheng Liu.  In Proceedings of the 1st IEEE & IFIP International Symposium on Theoretical Aspects of Software Engineering (TASE2007), pages 117-126, Shanghai, China, Jun 2007. IEEE Computer Society.[ bib | .pdf ] 

2006

  1. Building Proof-Carrying Security Programs Based on Coq.  Li Guo, Yiyun Chen, Long Li, Zhaopeng Li.  Chinese Journal of Computer Engineering and Applications,42(21):64-67,73, July 2006

Copyright © 2003-2010, Zhaopeng Li, University of Science & Technology of China. Last modified: 16:56, May 24, 2010.

说明: Valid HTML 4.01 Transitional