|
6
|
1 @misc{golang_impl,
|
|
2
|
2 title = {josharian/impl},
|
|
6
|
3 howpublished = {\url{https://github.com/josharian/impl}},
|
|
|
4 }
|
|
|
5
|
|
56
|
6 @misc{javaimpl,
|
|
|
7 title = {Java implements Keyword},
|
|
|
8 howpublished = {\url{https://www.w3schools.com/java/ref_keyword_implements.asp}},
|
|
|
9 }
|
|
|
10
|
|
6
|
11 @misc{eclipse.jdt.ls,
|
|
|
12 title = {Eclipse JDT Language Server},
|
|
|
13 howpublished = {\url{https://github.com/eclipse/eclipse.jdt.ls}},
|
|
|
14 }
|
|
|
15
|
|
8
|
16 @misc{babel,
|
|
|
17 title = {Babel},
|
|
|
18 howpublished = {\url{https://babeljs.io/}},
|
|
|
19 }
|
|
32
|
20
|
|
57
|
21 @misc{cbcxv6repo,
|
|
|
22 title = {CbC\_xv6},
|
|
|
23 author = {並列信頼研究室},
|
|
|
24 organization = "琉球大学",
|
|
|
25 howpublished = {\url{http://www.cr.ie.u-ryukyu.ac.jp/hg/CbC/CbC_xv6/}},
|
|
|
26 note = {Accessed: 2021-02-02},
|
|
|
27 }
|
|
|
28
|
|
|
29 @misc{cbcgcc,
|
|
|
30 title = {CbC\_gcc},
|
|
|
31 author = {並列信頼研究室},
|
|
|
32 organization = "琉球大学",
|
|
|
33 howpublished = {\url{http://www.cr.ie.u-ryukyu.ac.jp/hg/CbC/CbC_gcc/}},
|
|
|
34 note = {Accessed: 2021-02-02},
|
|
|
35 }
|
|
|
36
|
|
|
37 @misc{cbcllvm,
|
|
|
38 title = {CbC\_llvm},
|
|
|
39 author = {並列信頼研究室},
|
|
|
40 organization = "琉球大学",
|
|
|
41 howpublished = {\url{http://www.cr.ie.u-ryukyu.ac.jp/hg/CbC/CbC_llvm/}},
|
|
|
42 note = {Accessed: 2021-02-02},
|
|
|
43 }
|
|
|
44
|
|
|
45
|
|
|
46
|
|
32
|
47 @misc{eclipse_pull322,
|
|
6
|
48 title = {Add unimplemented methods code action},
|
|
|
49 author = {yaohaizh},
|
|
2
|
50 organization = "GitHub",
|
|
6
|
51 url = {\url{https://github.com/eclipse/eclipse.jdt.ls/pull/322}},
|
|
2
|
52 refdate = "2021-01-21",
|
|
|
53 }
|
|
|
54
|
|
28
|
55 @misc{vscode-go,
|
|
2
|
56 title = {golang/vscode-go},
|
|
|
57 author = {golang},
|
|
|
58 organization = "GitHub",
|
|
|
59 url = {\url{https://github.com/golang/vscode-go}},
|
|
|
60 refdate = "2021-01-21",
|
|
|
61 }
|
|
|
62
|
|
28
|
63 @misc{rpi,
|
|
|
64 title = "{Raspberry Pi}",
|
|
|
65 howpublished = {https://www.raspberrypi.org}
|
|
|
66 }
|
|
|
67
|
|
|
68 @misc{xv6rpi,
|
|
|
69 author = {Zhiyi Wang},
|
|
|
70 title = "{xv6-rpi}",
|
|
|
71 howpublished = "{\url{https://code.google.com/archive/p/xv6-rpi/}}",
|
|
|
72 year = {2013}
|
|
|
73 }
|
|
|
74
|
|
2
|
75 @article{
|
|
28
|
76 llvmcbc,
|
|
2
|
77 author = "Kaito TOKKMORI and Shinji KONO",
|
|
|
78 title = "Implementing Continuation based language in LLVM and Clang",
|
|
|
79 journal = "LOLA 2015",
|
|
|
80 month = "July",
|
|
|
81 year = 2015
|
|
|
82 }
|
|
|
83
|
|
28
|
84
|
|
|
85 @misc{Yang:2010:SLI:1806596.1806610,
|
|
|
86 author = {Yang, Jean and Hawblitzel, Chris},
|
|
|
87 title = {Safe to the Last Instruction: Automated Verification of a Type-safe Operating System},
|
|
|
88 booktitle = {Proceedings of the 31st ACM SIGPLAN Conference on Programming Language Design and Implementation},
|
|
|
89 series = {PLDI '10},
|
|
|
90 year = {2010},
|
|
|
91 isbn = {978-1-4503-0019-3},
|
|
|
92 location = {Toronto, Ontario, Canada},
|
|
|
93 pages = {99--110},
|
|
|
94 numpages = {12},
|
|
|
95 doi = {10.1145/1806596.1806610},
|
|
|
96 acmid = {1806610},
|
|
|
97 publisher = {ACM},
|
|
|
98 address = {New York, NY, USA},
|
|
|
99 keywords = {operating system, run-time system, type safety, verification},
|
|
|
100 }
|
|
|
101
|
|
|
102 @misc{Klein:2009:SFV:1629575.1629596,
|
|
|
103 author = {Klein, Gerwin and Elphinstone, Kevin and Heiser, Gernot and Andronick, June and Cock, David and Derrin, Philip and Elkaduwe, Dhammika and Engelhardt, Kai and Kolanski, Rafal and Norrish, Michael and Sewell, Thomas and Tuch, Harvey and Winwood, Simon},
|
|
|
104 title = {seL4: Formal Verification of an OS Kernel},
|
|
|
105 booktitle = {Proceedings of the ACM SIGOPS 22Nd Symposium on Operating Systems Principles},
|
|
|
106 series = {SOSP '09},
|
|
|
107 year = {2009},
|
|
|
108 isbn = {978-1-60558-752-3},
|
|
|
109 location = {Big Sky, Montana, USA},
|
|
|
110 pages = {207--220},
|
|
|
111 numpages = {14},
|
|
|
112 doi = {10.1145/1629575.1629596},
|
|
|
113 acmid = {1629596},
|
|
|
114 publisher = {ACM},
|
|
|
115 address = {New York, NY, USA},
|
|
|
116 keywords = {isabelle/hol, l4, microkernel, sel4},
|
|
|
117 }
|
|
|
118
|
|
|
119 @article{Sigurbjarnarson:2016:PVF:3026877.3026879,
|
|
|
120 author = {Sigurbjarnarson, Helgi and Bornholt, James and Torlak, Emina and Wang, Xi},
|
|
|
121 title = {Push-button Verification of File Systems via Crash Refinement},
|
|
|
122 booktitle = {Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation},
|
|
|
123 series = {OSDI'16},
|
|
|
124 year = {2016},
|
|
|
125 isbn = {978-1-931971-33-1},
|
|
|
126 location = {Savannah, GA, USA},
|
|
|
127 pages = {1--16},
|
|
|
128 numpages = {16},
|
|
|
129 acmid = {3026879},
|
|
|
130 publisher = {USENIX Association},
|
|
|
131 address = {Berkeley, CA, USA},
|
|
|
132 }
|
|
|
133
|
|
|
134
|
|
|
135
|
|
|
136 @article{
|
|
|
137 hyperKernel,
|
|
|
138 author = {Nelson, Luke and Sigurbjarnarson, Helgi and Zhang, Kaiyuan and Johnson, Dylan and Bornholt, James and Torlak, Emina and Wang, Xi},
|
|
|
139 title = {Hyperkernel: Push-Button Verification of an OS Kernel},
|
|
|
140 journal = {Proceedings of the 26th Symposium on Operating Systems Principles},
|
|
|
141 year = 2017
|
|
|
142 }
|
|
|
143
|
|
|
144
|
|
|
145
|
|
|
146 @article{
|
|
|
147 agda-ryokka,
|
|
29
|
148 author = "外間政尊 and 河野真治",
|
|
|
149 title = "GearsOS の Hoare Logic をべースにした検証手法",
|
|
28
|
150 journal = "ソフトウェアサイエンス研究会",
|
|
|
151 month = "Jan",
|
|
|
152 year = 2019
|
|
|
153 }
|
|
|
154
|
|
|
155 @article{agda,
|
|
|
156 author = {Norell, Ulf},
|
|
|
157 title = {Dependently Typed Programming in Agda},
|
|
|
158 booktitle = {Proceedings of the 4th International Workshop on Types in Language Design and Implementation},
|
|
|
159 series = {TLDI '09},
|
|
|
160 year = {2009},
|
|
|
161 isbn = {978-1-60558-420-1},
|
|
|
162 location = {Savannah, GA, USA},
|
|
|
163 pages = {1--2},
|
|
|
164 numpages = {2},
|
|
|
165 doi = {10.1145/1481861.1481862},
|
|
|
166 acmid = {1481862},
|
|
|
167 publisher = {ACM},
|
|
|
168 address = {New York, NY, USA},
|
|
|
169 keywords = {dependent types, programming},
|
|
|
170 }
|
|
|
171
|
|
|
172 @InProceedings{llvm,
|
|
|
173 author = {Chris Lattner and Vikram Adve},
|
|
|
174 title = "{LLVM: A Compilation Framework for Lifelong Program Analysis \& Transformation}",
|
|
|
175 booktitle = "{Proceedings of the 2004 International Symposium on Code Generation and Optimization (CGO'04)}",
|
|
|
176 address = {Palo Alto, California},
|
|
|
177 month = {Mar},
|
|
|
178 year = {2004}
|
|
|
179 }
|
|
|
180
|
|
30
|
181 @manual{coq,
|
|
|
182 author = "{the coq proof assistant}",
|
|
|
183 title ="{\url{https://coq.inria.fr/}}",
|
|
|
184 }
|
|
|
185
|
|
28
|
186 @manual{gcc,
|
|
|
187 author = "{GNU Compiler Collection (GCC) Internals}",
|
|
|
188 title ="{\url{http://gcc.gnu.org/onlinedocs/gccint/}}",
|
|
|
189 }
|
|
|
190
|
|
|
191 @article{weko_195888_1,
|
|
|
192 author = "坂本 昂弘 and 桃原 優 and 河野 真治",
|
|
|
193 title = "継続を用いたx.v6 kernelの書き換え",
|
|
|
194 year = "2019",
|
|
|
195 institution = "琉球大学工学部情報工学科, 琉球大学大学院理工学研究科情報工学専攻, 琉球大学工学部情報工学科",
|
|
|
196 journal = "情報処理学会システムソフトウェアとオペレーティング・システム研究会(OS)",
|
|
|
197 number = "4",
|
|
|
198 month = "may"
|
|
|
199 }
|
|
|
200
|
|
|
201 @article{weko_82695_1,
|
|
|
202 author = "大城 信康 and 河野 真治",
|
|
|
203 title = "ContinuationbasedCのGCC4.6上の実装について",
|
|
|
204 journal = "第53回プログラミング・シンポジウム予稿集",
|
|
|
205 year = "2012",
|
|
|
206 volume = "2012",
|
|
|
207 number = "",
|
|
|
208 pages = "69--78",
|
|
|
209 month = "jan"
|
|
|
210 }
|
|
|
211
|
|
|
212
|
|
|
213
|
|
|
214 @article{
|
|
|
215 gears,
|
|
|
216 author = "河野 真治 and 伊波 立樹 and 東恩納 琢偉",
|
|
29
|
217 title = "Code Gear、Data Gear に基づく OS のプロトタイプ",
|
|
28
|
218 journal = "情報処理学会システムソフトウェアとオペレーティング・システム研究会(OS)",
|
|
|
219 month = "May",
|
|
|
220 year = 2016
|
|
|
221 }
|
|
|
222
|
|
|
223 @misc{xv6,
|
|
|
224 author = "{Russ Cox, Frans Kaashoek, Robert Morris}",
|
|
|
225 title = {xv6 a simple, Unix-like teaching operating system},
|
|
|
226 howpublished = {\url{https://pdos.csail.mit.edu/6.828/2018/xv6/book-rev11.pdf}},
|
|
|
227 }
|
|
|
228
|
|
|
229
|
|
|
230 @article{Chen:2015:UCH:2815400.2815402,
|
|
|
231 author = {Chen, Haogang and Ziegler, Daniel and Chajed, Tej and Chlipala, Adam and Kaashoek, M. Frans and Zeldovich, Nickolai},
|
|
|
232 title = {Using Crash Hoare Logic for Certifying the FSCQ File System},
|
|
|
233 booktitle = {Proceedings of the 25th Symposium on Operating Systems Principles},
|
|
|
234 series = {SOSP '15},
|
|
|
235 year = {2015},
|
|
|
236 isbn = {978-1-4503-3834-9},
|
|
|
237 location = {Monterey, California},
|
|
|
238 pages = {18--37},
|
|
|
239 numpages = {20},
|
|
|
240 doi = {10.1145/2815400.2815402},
|
|
|
241 acmid = {2815402},
|
|
|
242 publisher = {ACM},
|
|
|
243 address = {New York, NY, USA},
|
|
|
244 }
|
|
|
245
|
|
|
246 @book{lions1996lions,
|
|
|
247 title={Lions' Commentary on UNIX 6th Edition with Source Code},
|
|
|
248 author={Lions, J.},
|
|
|
249 isbn={9781573980135},
|
|
|
250 lccn={55015401},
|
|
|
251 series={Computer classics revisited},
|
|
|
252 url={https://books.google.co.jp/books?id=OlZ3QgAACAAJ},
|
|
|
253 year={1996},
|
|
|
254 publisher={Peer-to-Peer Communications}
|
|
|
255 }
|
|
|
256
|
|
|
257
|
|
|
258
|
|
|
259
|
|
|
260 @misc{moggi-monad,
|
|
2
|
261 author = {Moggi, Eugenio},
|
|
|
262 title = {Notions of Computation and Monads},
|
|
|
263 journal = {Inf. Comput.},
|
|
|
264 issue_date = {July 1991},
|
|
|
265 volume = {93},
|
|
|
266 number = {1},
|
|
|
267 month = jul,
|
|
|
268 year = {1991},
|
|
|
269 issn = {0890-5401},
|
|
|
270 pages = {55--92},
|
|
|
271 numpages = {38},
|
|
|
272 doi = {10.1016/0890-5401(91)90052-4},
|
|
|
273 acmid = {116984},
|
|
|
274 publisher = {Academic Press, Inc.},
|
|
|
275 address = {Duluth, MN, USA},
|
|
|
276 }
|
|
|
277
|
