Languages

Biblio

Conference Paper
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)
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)
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.
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.
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)
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)
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)
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)
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)
Li Z, Zhang Y, Chen Y.  2011.  A Method to Generate Verification Condition Generator. Fifth International Conference on Theoretical Aspects of Software Engineering.
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)
Guo Y, Feng X, Shao Z, Shi P.  2012.  Modular Verification of Concurrent Thread Management. 10th Asian Symposium on Programming Languages and Systems.
Liang H, Feng X.  2013.  Modular Verification of Linearizability with Non-Fixed Linearization Points. 34th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'13).
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)
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)
Zhang Y, Feng X.  2013.  An Operational Approach to Happens-before Memory Model. The 7th International Symposium on Theoretical Aspects of Software Engineering (TASE '13).
Xu F, Fu M, Feng X, Zhang X, Zhang H, Li Z.  2016.  A Practical Verification Framework for Preemptive OS Kernels. Proc. 28th International Conference on Computer Aided Verification (CAV’16), part II, pages 59--79.
Liang H, Feng X.  2016.  A Program Logic for Concurrent Objects under Fair Scheduling. Proc. 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2016), pp 385-399.
Liang H, Feng X, Fu M.  2014.  Rely-Guarantee-Based Simulation for Compositional Verification of Concurrent Program Transformations. ACM Transactions on Programming Languages and Systems (TOPLAS), 36(1), pp 3:1-3:55.
Liang H, Feng X, Fu M.  2012.  A Rely-Guarantee-Based Simulation for Verifying Concurrent Program Transformations. 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'12).