Languages

Biblio

2016
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.
2015
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.
2014
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.
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.
2013
Li Z, Zhang Y, Chen Y.  2013.  A shape graph logic and a shape system. Journal of Computer Science and Technology. 28(6)
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).
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).
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).
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)
2012
Zhang Z, Feng X, Fu M, Shao Z, Li Y.  2012.  A Structural Approach to Prophecy Variables. 9th annual conference on Theory and Applications of Models of Computation.
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, 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).
2011
Li Z, Zhang Y, Chen Y.  2011.  A Method to Generate Verification Condition Generator. Fifth International Conference on Theoretical Aspects of Software Engineering.
Wang W, Shao Z, Jiang X, Guo Y.  2011.  A Simple Model for Certifying Assembly Programs with First-class Function Pointers. 5th IEEE International Symposium on Theoretical Aspects of Software Engineering.
2010
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)
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)
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)
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)
2009
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.
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 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.  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.  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)