Languages

Biblio

2008
Feng X, Shao Z, Guo Y, Dong Y.  2008.  Combining Domain-Specific and Foundational Logics to Verify Complete Software Systems. Second IFIP Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE'08). :54-69. Download: itrimp.pdf (250.73 KB)
Guo Y, Chen Y, Lin C.  2008.  A Method for Code Safety Proof Construction. Chinese Journal of Software. 19:2720-2727. Download: guo08jos.pdf (74.08 KB)
Li Z, Chen Y, Ge L, Hua B.  2008.  A Formal Certifying Framework for Assembly Programs. Chinese Journal of Computer Research and Development. 45:825-833. Download: li08jcrd.pdf (932.37 KB)
Chen Y, Hua B, Ge L, Wang Z.  2008.  A Pointer Logic for Safety Verification of Pointer Programs. Chinese Journal of Computers. 31:372-380. Download: chen08joc.pdf (419.05 KB)
Feng X, Shao Z, Dong Y, Guo Y.  2008.  Certifying Low-Level Programs with Hardware Interrupts and Preemptive Threads. Proceedings of the 2008 ACM SIGPLAN conference on Programming Language Design and Implementation (PLDI 2008). :170-182. Download: aim.pdf (291.12 KB)
Wang Z, Chen Y, Wang Z, Wang W, Tian B.  2008.  An Extension to Pointer Logic for Verification. Proceedings of 2nd IEEE IFIP International Symposium on Theoretical Aspects of Software Engineering (TASE 2008). :49-56. Download: wang08tase.pdf (161.61 KB)
Hua B, Chen Y, Li Z, Wang Z, Ge L.  2008.  Design and Proof of a Safe Programming Language {P}ointer{C}. Chinese Journal of Computers. 31:556-564. Download: hua08joc.pdf (432.84 KB)
2007
Gao Y, Chen Y.  2007.  A Comparable Code Obfuscation Framework Measuring Efficiency Based on Abstract Interpretation. Chinese Journal of Computers. 30:806-814. Download: gao07joc.pdf (485.94 KB)
Lin C, Chen Y, Li L, Hua B.  2007.  Garbage Collector Verification for Proof-Carrying Code. Journal of Computer Science and Technology. 22:426-437. Download: paper.pdf (307.85 KB)
Guo Y, Jiang X, Chen Y, Lin C.  2007.  A Certified Thread Library for Multithreaded User Programs. Proceedings of 1st IEEE IFIP International Symposium on Theoretical Aspects of Software Engineering (TASE 2007). :127-136. Download: guo07tase.pdf (319.29 KB)
Chen Y, Ge L, Hua B, Li Z, Liu C.  2007.  Design of a Certifying Compiler Supporting Proof of Program Safety. Proceedings of 1st IEEE IFIP International Symposium on Theoretical Aspects of Software Engineering (TASE 2007). :117-126. Download: dccspps.pdf (143.71 KB)
Lin C, McCreight A, Shao Z, Chen Y, Guo Y.  2007.  Foundational Typed Assembly Language with Certified Garbage Collection. Proceedings of 1st IEEE IFIP International Symposium on Theoretical Aspects of Software Engineering (TASE 2007). :326-335. Download: talgc.pdf (207.19 KB)
McCreight A, Shao Z, Lin C, Li L.  2007.  A General Framework for Certifying Garbage Collectors and Their Mutators. Proceedings of the 2007 ACM SIGPLAN conference on Programming Language Design and Implementation (PLDI 2007). :468-479. Download: hgc.pdf (273.09 KB)
Chen Y, Ge L, Hua B, Li Z, Liu C, Wang Z.  2007.  A Pointer Logic and Certifying Compiler. Frontiers of Computer Science in China. 1:297-312. Download: chen07fcs.pdf (1.53 MB)
Feng X, Ni Z, Shao Z, Guo Y.  2007.  An Open Framework for Foundational Proof-Carrying Code. Proceedings of the 3rd ACM Workshop on Types in Language Design and Implementation. :67-78. Download: ocap.pdf (265.54 KB)
Xiang S, Chen Y, Lin C, Li L.  2007.  Coq Implementation of Certified Dynamic Storage Allocation. Chinese Journal of Computer Research and Development. 44:361-367. Download: xiang07jcrd.pdf (432.33 KB)
2006
Xiang S, Chen Y, Lin C, Li L.  2006.  Modularly Certified Dynamic Storage Allocation in SCAP. Proceedings of Sixth International Conference on Quality Software (QSIC'06). :321-328. Download: xiang06qsic.pdf (325.81 KB)
Chen H, Chen Y, Wu P, Xiang S.  2006.  A Typed Low-Level Language Used in Java Virtual Machine. Chinese Journal of Computer Research and Development. 43:15-22. Download: chen06jcrd.pdf (382.24 KB)
Feng X, Shao Z, Vaynberg A, Xiang S, Ni Z.  2006.  Modular Verification of Assembly Code with Stack-Based Control Abstractions. Proceedings of the 2006 ACM SIGPLAN conference on Programming Language Design and Implementation. :401-414. Download: sbca.pdf (315.19 KB)
Wu P, Chen Y, Zhang J.  2006.  Static Data-Race Detection for Multithread Programs. Chinese Journal of Computer Research and Development. 43:329-335.
Fu X, Zhang Y, Chen Y.  2006.  Data-Layout Optimization Using Reuse Distance Distribution. Emerging Directions in Embedded and Ubiquitous Computing EUC 2006 Workshops: NCUS, SecUbiq, USN, TRUST, ESO, and MSA. 4097:858-867. Download: fu06.pdf (234.69 KB)
2005
Wu P, Chen Y, Zhang J.  2005.  Effective Synchronization Removal in Concurrent Java Programs. Chinese Journal of Software. 16:1708-1716. Download: wu05jos.pdf (224.66 KB)
Chen H, Chen Y, Ru X.  2005.  A Tag Type For Certifying Compilation of Java Program. Chinese Journal of Software. 16:346-354. Download: chen05jos.pdf (511.59 KB)