Languages

Biblio

2005
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)
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)
2006
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)
Wu P, Chen Y, Zhang J.  2006.  Static Data-Race Detection for Multithread Programs. Chinese Journal of Computer Research and Development. 43:329-335.
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)
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)
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)
2007
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)
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)
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)
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)
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)
2008
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)
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)
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)
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)
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)
2009
Li L, Zhang Y, Chen Y, Li Y.  2009.  Certifying concurrent programs using transactional memory. Journal of Computer Science and Technology. 24:121. Download: jcst0901.pdf (467.14 KB); impl.rar (75.93 KB)
Fu M, Zhang Y, Li Y.  2009.  Formal reasoning about concurrent assembly code with reentrant locks. 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering(TASE 2009).  Download: tase2009.pdf (89.95 KB); impl.rar (50.53 KB)