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 
certifying compiler
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)
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)
concurrent program safety
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)
concurrent separation logic
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)
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)
context
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)
Hoare logic
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)
incremental gargabge collector
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.
mutual exclusive locks
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)
Pointer Logic
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)
program
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)
program logic
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)
program safety
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)
program verification
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.
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)
proof-carrying code
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)
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)
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)
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.
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)
proofcarrying code
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)
read-write locks
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)
reentrant locks
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)
safety
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)