@article{ gears, author = "河野 真治 and 伊波 立樹 and 東恩納 琢偉", title = "Code Gear、Data Gear に基づく OS のプロトタイプ", journal = "情報処理学会システムソフトウェアとオペレーティング・システム研究会(OS)", month = "May", year = 2016 } @article{ cbc, author = "Kaito TOKKMORI and Shinji KONO", title = "Implementing Continuation based language in LLVM and Clang", journal = "LOLA 2015", month = "July", year = 2015 } @article{ llvm, title = "LLVM documentation.", howpublished = "{http://llvm.org/docs/index.html}" } @article{ SMT1, author = "Gerwin Klein, June Andronick, Kevin Elphinstone, Toby Murray, Thomas Sewell, Rafal Kolanski, Rafal Kolanski, Gernot Heiser" title = "Comprehensive Formal Verification of an OS Microkernel" journal = "ACM Transactions on Computer Systems (TOCS) 32.1" year = 2014 } @article{ SMT2, author = "Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, Simon Winwood" title = "seL4: Formal Verification of an OS Kernel" journal = "Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles. ACM" year = 2009 } @article{ type, author = "Jean Yang, Chris Hawblitzel" title = "Safe to the Last Instruction: Automated Verification of a Type-Safe Operating System" journal = "ACM Sigplan Notices. Vol. 45. No. 6. ACM" year = 2010 } @article{ , author = "Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan (Newman) Wu, Jieung Kim, Vilhelm Sjo ̈berg, David Costanzo" title = "CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels" journal = "OSDI" year = 2016 } @article{ , author = "Helgi Sigurbjarnarson, James Bornholt, Emina Torlak, Xi Wang" title = "Push-Button Verification of File Systems via Crash Refinement" journal = "OSDI" year = 2016 } @article{ , author = "Luke Nelson, Helgi Sigurbjarnarson, Kaiyuan Zhang, Dylan Johnson, James Bornholt, Emina Torlak, and Xi Wang" title = "Hyperkernel: Push-Button Verification of an OS Kernel" journal = "Proceedings of the 26th Symposium on Operating Systems Principles. ACM" year = 2017 } @article{ , author = "Haogang Chen, Daniel Ziegler, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, Nickolai Zeldovich" title = "Using Crash Hoare Logic for Certifying the FSCQ File System" journal = "Proceedings of the 25th Symposium on Operating Systems Principles. ACM" year = 2015 }