seL4

1. TPHOLs

   Secure Microkernels, State Monads and Scalable Refinement Cock, David, Klein, Gerwin, and Sewell, Thomas In Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings 2008
2. SOSP

   seL4: formal verification of an OS kernel Klein, Gerwin, Elphinstone, Kevin, Heiser, Gernot, Andronick, June, Cock, David, Derrin, Philip, Elkaduwe, Dhammika, Engelhardt, Kai, Kolanski, Rafal, Norrish, Michael, Sewell, Thomas, Tuch, Harvey, and Winwood, Simon In Proceedings of the 22nd ACM Symposium on Operating Systems Principles 2009, SOSP 2009, Big Sky, Montana, USA, October 11-14, 2009 2009
3. ITP

   seL4 Enforces Integrity Sewell, Thomas, Winwood, Simon, Gammie, Peter, Murray, Toby C., Andronick, June, and Klein, Gerwin In Interactive Theorem Proving - Second International Conference, ITP 2011, Berg en Dal, The Netherlands, August 22-25, 2011. Proceedings 2011
4. IEEE S&P

   seL4: From General Purpose to a Proof of Information Flow Enforcement Murray, Toby C., Matichuk, Daniel, Brassil, Matthew, Gammie, Peter, Bourke, Timothy, Seefried, Sean, Lewis, Corey, Gao, Xin, and Klein, Gerwin In 2013 IEEE Symposium on Security and Privacy, SP 2013, Berkeley, CA, USA, May 19-22, 2013 2013
5. PLDI

   Translation validation for a verified OS kernel Sewell, Thomas Arthur Leck, Myreen, Magnus O., and Klein, Gerwin In ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’13, Seattle, WA, USA, June 16-19, 2013 2013
6. TOCS

   Comprehensive formal verification of an OS microkernel Klein, Gerwin, Andronick, June, Elphinstone, Kevin, Murray, Toby C., Sewell, Thomas, Kolanski, Rafal, and Heiser, Gernot ACM Trans. Comput. Syst. 2014
7. Phil. Trans.

   Provably trustworthy systems Klein, Gerwin, Andronick, June, Keller, Gabriele, Matichuk, Daniel, Murray, Toby, and O’Connor, Liam Philosophical Transactions of The Royal Society A Mathematical Physical and Engineering Sciences 2017
8. ITP

   Program Verification in the Presence of Cached Address Translation Syeda, Hira Taqdees, and Klein, Gerwin In Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings 2018

CertiKOS

1. POPL

   Deep Specifications and Certified Abstraction Layers Gu, Ronghui, Koenig, Jérémie, Ramananandro, Tahina, Shao, Zhong, Wu, Xiongnan (Newman), Weng, Shu-Chun, Zhang, Haozhong, and Guo, Yu In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015 2015
2. PLDI

   Toward compositional verification of interruptible OS kernels and device drivers Chen, Hao, Wu, Xiongnan (Newman), Shao, Zhong, Lockerman, Joshua, and Gu, Ronghui In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, Santa Barbara, CA, USA, June 13-17, 2016 2016
3. PLDI

   End-to-end verification of information-flow security for C and assembly programs Costanzo, David, Shao, Zhong, and Gu, Ronghui In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, Santa Barbara, CA, USA, June 13-17, 2016 2016
4. OSDI

   CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels Gu, Ronghui, Shao, Zhong, Chen, Hao, Wu, Xiongnan (Newman), Kim, Jieung, Sjöberg, Vilhelm, and Costanzo, David In 12th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2016, Savannah, GA, USA, November 2-4, 2016 2016
5. PLDI

   Certified concurrent abstraction layers Gu, Ronghui, Shao, Zhong, Kim, Jieung, Wu, Xiongnan (Newman), Koenig, Jérémie, Sjöberg, Vilhelm, Chen, Hao, Costanzo, David, and Ramananandro, Tahina In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, Philadelphia, PA, USA, June 18-22, 2018 2018
6. CAV

   Integrating Formal Schedulability Analysis into a Verified OS Kernel Guo, Xiaojie, Lesourd, Maxime, Liu, Mengqi, Rieg, Lionel, and Shao, Zhong In Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part II 2019
7. OSDI

   CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels Gu, Ronghui, Shao, Zhong, Chen, Hao, Wu, Xiongnan (Newman), Kim, Jieung, Sjöberg, Vilhelm, and Costanzo, David In 12th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2016, Savannah, GA, USA, November 2-4, 2016 2016
8. LICS

   Refinement-Based Game Semantics for Certified Abstraction Layers Koenig, Jérémie, and Shao, Zhong In LICS ’20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, July 8-11, 2020 2020
9. POPL

   Virtual timeline: a formal abstraction for verifying preemptive schedulers with temporal isolation Liu, Mengqi, Rieg, Lionel, Shao, Zhong, Gu, Ronghui, Costanzo, David, Kim, Jung-Eun, and Yoon, Man-Ki Proc. ACM Program. Lang. 2020

其它

1. CAV

   A Practical Verification Framework for Preemptive OS Kernels Xu, Fengwei, Fu, Ming, Feng, Xinyu, Zhang, Xiaoran, Zhang, Hui, and Li, Zhaohui In Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part II 2016
2. ICECCS

   A Formally Verified Buddy Memory Allocation Model Jiang, Ke, Sanán, David, Zhao, Yongwang, Kan, Shuanglong, and Liu, Yang In 24th International Conference on Engineering of Complex Computer Systems, ICECCS 2019, Guangzhou, China, November 10-13, 2019 2019
3. SETTA

   A Verified Specification of TLSF Memory Management Allocator Using State Monads Zhang, Yu, Zhao, Yongwang, Sanán, David, Qiao, Lei, and Zhang, Jinkun In Dependable Software Engineering. Theories, Tools, and Applications - 5th International Symposium, SETTA 2019, Shanghai, China, November 27-29, 2019, Proceedings 2019
4. TDSC

   Refinement-Based Specification and Security Analysis of Separation Kernels Zhao, Yongwang, Sanán, David, Zhang, Fuyuan, and Liu, Yang IEEE Trans. Dependable Secur. Comput. 2019
5. CAV

   Rely-Guarantee Reasoning About Concurrent Memory Management in Zephyr RTOS Zhao, Yongwang, and Sanán, David In Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part II 2019
6. SOSP

   Using concurrent relational logic with helpers for verifying the AtomFS file system Zou, Mo, Ding, Haoran, Du, Dong, Fu, Ming, Gu, Ronghui, and Chen, Haibo In Proceedings of the 27th ACM Symposium on Operating Systems Principles, SOSP 2019, Huntsville, ON, Canada, October 27-30, 2019 2019