Special Issue: Software Systems
|  Xu F, Fu M, Feng X, Zhang X, Zhang H, Li Z. A practical verification framework for preemptive OS kernels. In Proc. the 28th International Conference, July 2016, pp.59-79.
 Klein G, Elphinstone K, Heiser G, Andronick J, Cock D, Derrin P, Elkaduwe D, Engelhardt K, Kolanski R, Norrish M, Sewell T, Tuch H, Winwood S. seL4:Formal verification of an OS Kernel. In Proc. the 22nd ACM Symposium on Operating Systems Principles, Oct. 2009, pp.207-220.
 Gu R, Koenig J, Ramananandro T, Shao Z, Wu X N, Weng S C, Zhang H, Guo Y. Deep specifications and certified abstraction layers. In Proc. the 42nd Annual ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, Jan. 2015, pp.59-5608.
 Zha J, Feng X, Qiao L. Modular verification of SPARCv8 code. In Proc. the 16th Asian Symposium on Programming Languages and Systems, December 2018, pp.245-263.
 Feng X, Shao Z, Vaynberg A, Xiang S, Ni Z. Modular verification of assembly code with stack-based control abstractions. In Proc. the ACM SIGPLAN 2006 Conference on Programming Language Design and Implementation, June 2006, pp.401-414.
 Leroy X, Blazy S. Formal verification of a C-like memory model and its uses for verifying program transformations. Journal of Automated Reasoning, 2008, 41(1):1-31.
 Wang J, Fu M, Qiao L, Feng X. Formalizing SPARCv8 instruction set architecture in Coq. In Proc. the 3rd International Symposium on Dependable Software Engineering:Theories, Tools, and Applications, Oct. 2017, pp.300-316.
 Reynolds J. Separation logic:A logic for shared mutable data structures. In Proc. the 17th IEEE Symposium on Logic in Computer Science, July 2002, pp.55-74.
 Liang H, Feng X, Shao Z. Compositional verification of termination-preserving refinement of concurrent programs. In Proc. the Joint Meeting of the 23rd EACSL Annual Conference on Computer Science Logic and the 29th Annual ACM/IEEE Symposium on Logic in Computer Science, July 2014, Article No. 65.
 Necula G C, Lee P. Safe kernel extensions without run-time checking. In Proc. the 2nd USENIX Symp. Operating System Design and Implementation, October 1996, pp.229-243.
 Appel A W. Foundational proof-carrying code. In Proc. the 16th Annual IEEE Symposium on Logic in Computer Science, June 1998, pp.247-256.
 Morrisett G, Crary K, Glew N, Grossman D, Samuels R, Smith F, Walker D, Weirich S, Zdancewic S. TALx86:A realistic typed assembly language. In Proc. the 1999 ACM SIGPLAN Workshop on Compiler Support for System Software, May 1996, pp.25-35.
 Morrisett G, Walker D, Crary K, Glew N. From system F to typed assembly language. In Proc. the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Jan. 1998, pp.85-97.
 Yu D, Nadeem A H, Shao Z. Building certified libraries for PCC:Dynamic storage allocation. Science of Computer Programming, 2004, 50(1/2/3):101-127.
 Ni Z, Shao Z. Certified assembly programming with embedded code pointers. In Proc. the 33rd ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, January 2006, pp.320-333.
 Tan G, Appel A W. A compositional logic for control flow. In Proc. the 7th International Conference on Verification, Model Checking, and Abstract Interpretation, Jan. 2006, pp.80-94.
 Myreen M O, Gordon M J. Hoare logic for realistically modelled machine code. In Proc. the 13th International Conference on Tools and Algorithms for Construction and Analysis of Systems, March 2007, pp.568-582.
 Hou Z, Sanán D, Tiu A, Liu Y, Hoa K C. An executable formalisation of the SPARCv8 instruction set architecture:A case study for the LEON3 processor. In Proc. the 21st International Symposium on Formal Methods, November 2016, pp.388-405.
 Ni Z, Yu D, Shao Z. Using XCAP to certify realistic systems code:Machine context management. In Proc. the 20th International Conference on Theorem Proving in Higher Order Logics, Sept. 2007, pp.189-206.
 Yang J, Hawblitzel C. Safe to the last instruction:Automated verification of a type-safe operating system. In Proc. the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation, June 2010, pp.99-110.
 Berdine J, Calcagno C, O'Hearn P W. Symbolic execution with separation logic. In Proc. the 3rd Asian Symposium on Programming Languages and Systems, November 2005, pp.52-68.
 Berdine J, Calcagno C, O'Hearn P W. Smallfoot:Modular automatic assertion checking with separation logic. In Proc. the 4th International Symposium on Formal Methods for Components and Objects, November 2005, pp.115-137.
|||Wen-Jun Shi, Qin-Xiang Cao, Yu-Xin Deng, Han-Ru Jiang, Yuan Feng. Symbolic Reasoning About Quantum Circuits in Coq [J]. Journal of Computer Science and Technology, 2021, 36(6): 1291-1306.|
|||Zhi Ma, Lei Qiao, Meng-Fei Yang, Shao-Feng Li, Jin-Kun Zhang. Verification of Real Time Operating System Exception Management Based on SPARCv8 [J]. Journal of Computer Science and Technology, 2021, 36(6): 1367-1387.|
|||Yu Guo(郭 宇), Xin-Yu Jiang(蒋信予), and Yi-Yun Chen(陈意云). Certification of Thread Context Switching [J]. , 2010, 25(4): 827-840.|