Languages

Home

Biblio

A B C D E F G H I J K L M N O P Q R S T U V W X Y Z 
C
Chen, Y, Li Z, Wang Z, Hua B.  2010.  A Pointer Logic for Verification of Pointer Programs. Chinese Journal of Software. Vol.21(No.3):124-137. Download: chen09jos.pdf (313.82 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)
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)
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)
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)
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)
F
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)
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)
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)
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)
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)
Fu, M, Zhang Y, Li Y.  2010.  Formal verification of concurrent programs with read-write locks. Frontiers of Computer Science in China. 4(1):13. Download: paper.pdf (317.3 KB)ccprwl_impl.rar (44.96 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)
G
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)
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)
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)
H
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)
J
Jiang, X, Guo Y, Chen Y.  2009.  The Logical Approach to Low-level Stack Reasoning. 3th IEEE International Symposium on Theoretical Aspects of Software Engineering(TASE'09).  Download: tase-ieee.pdf (109.46 KB)
L
Li, Y, Zhang Y, Chen Y, Fu M.  2009.  On the verification of strong atomicity of programs using STM. 3rd IEEE International Conference on Secure Software Integration and Reliability Improvement(SSIRI2009).  Download: SSIRI2009.pdf (269 KB)coq-impl.rar (54.34 KB)
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)
Li, Y, Zhang Y, Chen Y, Fu M.  2009.  Formal reasoning about lazy-STM programs. submitted to Journal of Computer Science and Technology.  Download: Formal reasoning about lazy-STM programs.pdf (246.32 KB)coq-impl.rar (54.34 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)
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)
Lin, C, Chen Y, Hua B.  2009.  Verification of an Incremental Garbage Collector in Hoare-Style Logic. International Journal of Software and Informatics. 3(1):67-88.
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)