USTC-Yale Joint Research Center for High-Confidence Software

Recent Publications

[1] Yiyun Chen, Zhaopeng Li, Zhifang Wang, and Baojian Hua. A pointer logic for verification of pointer programs. Accepted by Chinese Journal of Software, 00(00):0000-0000, 00 2009. [ bib | .pdf ]

 

[2] Yu Guo, Yiyun Chen, and Chunxiao Lin. A method for code safety proof construction. Chinese Journal of Software, 19(10):2720-2727, Oct 2008. [ bib | .pdf ]

 

[3] Xinyu Feng, Zhong Shao, Yu Guo, and Yuan Dong. Combining Domain-Specific and Foundational Logics to Verify Complete Software Systems. In Second IFIP Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE'08), pages 54-69, Toronto, Canada, Oct 2008. Springer-Verlag. [ bib | .pdf ]

 

[4] Zhifang Wang, Yiyun Chen, Zhenming Wang, Wei Wang, and Bo Tian. An extension to pointer logic for verification. In Proceedings of 2nd IEEE IFIP International Symposium on Theoretical Aspects of Software Engineering (TASE 2008), pages 49-56, Nanjing, China, Jun 2008. IEEE Computer Society. [ bib | .pdf ]

 

[5] Xinyu Feng, Zhong Shao, Yuan Dong, and Yu Guo. Certifying low-level programs with hardware interrupts and preemptive threads. In Proceedings of the 2008 ACM SIGPLAN conference on Programming Language Design and Implementation (PLDI 2008), pages 170-182, Tucson, Arizona, Jun 2008. ACM Press. [ bib | .pdf ]

 

[6] Zhaopeng Li, Yiyun Chen, Lin Ge, and Baojian Hua. A formal certifying framework for assembly programs. Chinese Journal of Computer Research and Development, 45(5):825-833, May 2008. [ bib | .pdf ]

 

[7] Baojian Hua, Yiyun Chen, Zhaopeng Li, Zhifang Wang, and Lin Ge. Design and proof of a safe programming language PointerC. Chinese Journal of Computers, 31(4):556-564, April 2008. [ bib | .pdf ]

 

[8] Yiyun Chen, Baojian Hua, Lin Ge, and Zhifang Wang. A pointer logic for safety verification of pointer programs. Chinese Journal of Computers, 31(3):372-380, March 2008. [ bib | .pdf ]

 

[9] Yiyun Chen, Lin Ge, Baojian Hua, Zhaopeng Li, Cheng Liu, and Zhifang Wang. A pointer logic and certifying compiler. Frontiers of Computer Science in China, 1(3):297-312, Jul 2007. [ bib | .pdf ]

 

[10] Andrew McCreight, Zhong Shao, Chunxiao Lin, and Long Li. A general framework for certifying garbage collectors and their mutators. In Proceedings of the 2007 ACM SIGPLAN conference on Programming Language Design and Implementation (PLDI 2007), pages 468-479, San Diego, CA, USA, Jun 2007. ACM Press. [ bib | .pdf ]

 

[11] Yiyun Chen, Lin Ge, Baojian Hua, Zhaopeng Li, and Cheng Liu. Design of a certifying compiler supporting proof of program safety. In Proceedings of 1st IEEE IFIP International Symposium on Theoretical Aspects of Software Engineering (TASE 2007), pages 117-126, Shanghai, China, Jun 2007. IEEE Computer Society. [ bib | .pdf ]

 

[12] Yu Guo, Xinyu Jiang, Yiyun Chen, and Chunxiao Lin. A certified thread library for multithreaded user programs. In Proceedings of 1st IEEE IFIP International Symposium on Theoretical Aspects of Software Engineering (TASE 2007), pages 127-136, Shanghai, China, Jun 2007. IEEE Computer Society. [ bib | .pdf ]

 

[13] Chunxiao Lin, Andrew McCreight, Zhong Shao, Yiyun Chen, and Yu Guo. Foundational typed assembly language with certified garbage collection. In Proceedings of 1st IEEE IFIP International Symposium on Theoretical Aspects of Software Engineering (TASE 2007), pages 326-335, Shanghai, China, Jun 2007. IEEE Computer Society. [ bib | .pdf ]

 

[14] Ying Gao and Yiyun Chen. A comparable code obfuscation framework measuring efficiency based on abstract interpretation. Chinese Journal of Computers, 30(5):806-814, May 2007. [ bib | .pdf ]

 

[15] Chunxiao Lin, Yiyun Chen, Long Li, and Bei Hua. Garbage collector verification for proof-carrying code. Journal of Computer Science and Technology, 22(3):426-437, May 2007. [ bib | .pdf ]

 

[16] Sen Xiang, Yiyun Chen, Chunxiao Lin, and Long Li. Coq implementation of certified dynamic storage allocation. Chinese Journal of Computer Research and Development, 44(2):361-367, Feb 2007. [ bib | .pdf ]

 

[17] Xinyu Feng, Zhaozhong Ni, Zhong Shao, and Yu Guo. An open framework for foundational proof-carrying code. In Proceedings of the 3rd ACM Workshop on Types in Language Design and Implementation, pages 67-78, Nice, France, Jan 2007. ACM Press. [ bib | .pdf ]

 

[18] Sen Xiang, Yiyun Chen, Chunxiao Lin, and Long Li. Modularly certified dynamic storage allocation in scap. In Proceedings of Sixth International Conference on Quality Software (QSIC'06), pages 321-328, Beijing, China, Oct 2006. IEEE Computer Society. [ bib | .pdf ]

 

[19] Xiong Fu, Yu Zhang, and Yiyun Chen. Data-layout optimization using reuse distance distribution. In Emerging Directions in Embedded and Ubiquitous Computing EUC 2006 Workshops: NCUS, SecUbiq, USN, TRUST, ESO, and MSA, volume 4097 of Lecture Notes in Computer Science, pages 858-867, Seoul, Korea, Aug 2006. Springer. [ bib | .pdf ]

 

[20] Ping Wu, Yiyun Chen, and Jian Zhang. Static data-race detection for multithread programs. Chinese Journal of Computer Research and Development, 43(2):329-335, Feb 2006. [ bib ]

 

[21] Xinyu Feng, Zhong Shao, Alexander Vaynberg, Sen Xiang, and Zhaozhong Ni. Modular verification of assembly code with stack-based control abstractions. In Proceedings of the 2006 ACM SIGPLAN conference on Programming Language Design and Implementation, pages 401-414, Ottawa, Canada, Hone 2006. ACM Press. [ bib | .pdf ]

 

[22] Hui Chen, Yiyun Chen, Ping Wu, and Sen Xiang. A typed low-level language used in java virtual machine. Chinese Journal of Computer Research and Development, 43(1):15-22, Jan 2006. [ bib | .pdf ]

 

[23] Ping Wu, Yiyun Chen, and Jian Zhang. Effective synchronization removal in concurrent java programs. Chinese Journal of Software, 16(10):1708-1716, Oct 2005. [ bib | .pdf ]

 

[24] Hui Chen, Yiyun Chen, and Xiangmin Ru. A tag type for certifying compilation of java program. Chinese Journal of Software, 16(3):346-354, Mar 2005. [ bib | .pdf ]

 

This list has been generated by bibtex2html 1.88.