Languages

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 
A
Zhang Z, Li Z, Chen Y, Liu G.  2013.  An Automatic Program Verifier for PointerC: Design and Implementation. Journal of Computer Research and Development. 50(5)
C
Guo Y, Jiang X-Y, Chen Y-Y.  2010.  Cerification of Thread Context Switching. Journal of Computer Science and Technology. 25(4)(1):827-840. Download: swap.pdf (588.52 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)
Li Z, Zhuang Z, Chen Y, Yang S, Zhang Z, Fan D.  2010.  A Certifying Compiler for Clike Subset of C Language. 4th IEEE International Symposium on Theoretical Aspects of Software Engineering(TASE'2010). :47-56. Download: zpli_tase2010.pdf (459.9 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)
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)
Liang H, Hoffmann J, Feng X, Shao Z.  2013.  Characterizing Progress Properties of Concurrent Objects via Contextual Refinements. 24th International Conference on Concurrency Theory (CONCUR'13).
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)
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)
Liang H, Feng X, Shao Z.  2014.  Compositional Verification of Termination-Preserving Refinement of Concurrent Programs. Proc. Joint Meeting of the 23rd EACSL Annual Conference on Computer Science Logic and the 29th Annual ACM/IEEE Symposium on Logic in Computer Science (CSL-LICS'14). 2014.07.14-18. pp 65:1-65:10.
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)
D
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)
Gu R, Koenig J, Ramananandro T, Shao Z, Wu X(N), Weng S-C, Zhang H, Guo Y.  2015.  Deep Specifications and Certified Abstraction Layers. Proc. 42rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2015), pp 595-608.
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)
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)
E
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)
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)
F
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)
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)
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)
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)
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)
G
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)
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)
L
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)