|
Journal of Computer Science and Technology ›› 2020, Vol. 35 ›› Issue (6): 1382-1405.doi: 10.1007/s11390-020-0536-9
Special Issue: Software Systems
Previous Articles Next Articles
Jun-Peng Zha1,2, Xin-Yu Feng1,2,*, Member, CCF, ACM, and Lei Qiao3, Member, CCF
[1] 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. [2] 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. [3] 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. [4] 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. [5] 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. [6] 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. [7] 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. [8] 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. [9] 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. [10] 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. [11] Appel A W. Foundational proof-carrying code. In Proc. the 16th Annual IEEE Symposium on Logic in Computer Science, June 1998, pp.247-256. [12] 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. [13] 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. [14] 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. [15] 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. [16] 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. [17] 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. [18] 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. [19] 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. [20] 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. [21] 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. [22] 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. |
[1] | 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. |
[2] | 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. |
[3] | Yu Guo(郭 宇), Xin-Yu Jiang(蒋信予), and Yi-Yun Chen(陈意云). Certification of Thread Context Switching [J]. , 2010, 25(4): 827-840. |
|
|