--- a/Paper/prosym.bib	Sat Dec 23 00:51:46 2017 +0900
+++ b/Paper/prosym.bib	Sat Dec 23 11:52:17 2017 +0900
@@ -16,64 +16,31 @@
     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
-%}
+@InProceedings{llvm,
+author    = {Chris Lattner and Vikram Adve},
+title     = "{LLVM: A Compilation Framework for Lifelong Program Analysis \& Transformation}",
+booktitle = "{Proceedings of the 2004 International Symposium on Code Generation and Optimization (CGO'04)}",
+address   = {Palo Alto, California},
+month     = {Mar},
+year      = {2004}
+}
 
-%@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
-%}
+@inproceedings{Yang:2010:SLI:1806596.1806610,
+ author = {Yang, Jean and Hawblitzel, Chris},
+ title = {Safe to the Last Instruction: Automated Verification of a Type-safe Operating System},
+ booktitle = {Proceedings of the 31st ACM SIGPLAN Conference on Programming Language Design and Implementation},
+ series = {PLDI '10},
+ year = {2010},
+ isbn = {978-1-4503-0019-3},
+ location = {Toronto, Ontario, Canada},
+ pages = {99--110},
+ numpages = {12},
+ url = {http://doi.acm.org/10.1145/1806596.1806610},
+ doi = {10.1145/1806596.1806610},
+ acmid = {1806610},
+ publisher = {ACM},
+ address = {New York, NY, USA},
+ keywords = {operating system, run-time system, type safety, verification},
+}
 
-%@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
-%}