[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 SIGPLAN-SIGACT 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.
[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.
[15]
Ni Z, Shao Z. Certified assembly programming with embedded code pointers. In Proc. the 33rd ACM SIGPLAN-SIGACT 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.
京公网安备11010802044758号