0
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
1 @article{
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
2 cbc,
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
3 author = "Kaito TOKKMORI and Shinji KONO",
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
4 title = "Implementing Continuation based language in LLVM and Clang",
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
5 journal = "LOLA 2015",
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
6 month = "July",
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
7 year = 2015
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
8 }
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
9
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
10 @article{moggi-monad,
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
11 author = {Moggi, Eugenio},
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
12 title = {Notions of Computation and Monads},
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
13 journal = {Inf. Comput.},
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
14 issue_date = {July 1991},
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
15 volume = {93},
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
16 number = {1},
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
17 month = jul,
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
18 year = {1991},
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
19 issn = {0890-5401},
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
20 pages = {55--92},
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
21 numpages = {38},
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
22 url = {http://dx.doi.org/10.1016/0890-5401(91)90052-4},
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
23 doi = {10.1016/0890-5401(91)90052-4},
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
24 acmid = {116984},
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
25 publisher = {Academic Press, Inc.},
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
26 address = {Duluth, MN, USA},
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
27 }
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
28
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
29 @inproceedings{Yang:2010:SLI:1806596.1806610,
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
30 author = {Yang, Jean and Hawblitzel, Chris},
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
31 title = {Safe to the Last Instruction: Automated Verification of a Type-safe Operating System},
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
32 booktitle = {Proceedings of the 31st ACM SIGPLAN Conference on Programming Language Design and Implementation},
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
33 series = {PLDI '10},
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
34 year = {2010},
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
35 isbn = {978-1-4503-0019-3},
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
36 location = {Toronto, Ontario, Canada},
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
37 pages = {99--110},
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
38 numpages = {12},
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
39 url = {http://doi.acm.org/10.1145/1806596.1806610},
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
40 doi = {10.1145/1806596.1806610},
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
41 acmid = {1806610},
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
42 publisher = {ACM},
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
43 address = {New York, NY, USA},
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
44 keywords = {operating system, run-time system, type safety, verification},
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
45 }
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
46
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
47 @inproceedings{Klein:2009:SFV:1629575.1629596,
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
48 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},
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
49 title = {seL4: Formal Verification of an OS Kernel},
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
50 booktitle = {Proceedings of the ACM SIGOPS 22Nd Symposium on Operating Systems Principles},
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
51 series = {SOSP '09},
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
52 year = {2009},
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
53 isbn = {978-1-60558-752-3},
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
54 location = {Big Sky, Montana, USA},
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
55 pages = {207--220},
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
56 numpages = {14},
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
57 url = {http://doi.acm.org/10.1145/1629575.1629596},
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
58 doi = {10.1145/1629575.1629596},
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
59 acmid = {1629596},
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
60 publisher = {ACM},
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
61 address = {New York, NY, USA},
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
62 keywords = {isabelle/hol, l4, microkernel, sel4},
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
63 }
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
64
|
13
|
65 @article{Klein:2010:SFV:1743546.1743574,
|
|
66 author = {Klein, Gerwin and Andronick, June and Elphinstone, Kevin and Heiser, Gernot 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},
|
|
67 title = {seL4: Formal Verification of an Operating-system Kernel},
|
|
68 journal = {Commun. ACM},
|
|
69 issue_date = {June 2010},
|
|
70 volume = {53},
|
|
71 number = {6},
|
|
72 month = jun,
|
|
73 year = {2010},
|
|
74 issn = {0001-0782},
|
|
75 pages = {107--115},
|
|
76 numpages = {9},
|
|
77 url = {http://doi.acm.org/10.1145/1743546.1743574},
|
|
78 doi = {10.1145/1743546.1743574},
|
|
79 acmid = {1743574},
|
|
80 publisher = {ACM},
|
|
81 address = {New York, NY, USA},
|
|
82 }
|
|
83
|
|
84 @inproceedings{Nelson:2017:HPV:3132747.3132748,
|
|
85 author = {Nelson, Luke and Sigurbjarnarson, Helgi and Zhang, Kaiyuan and Johnson, Dylan and Bornholt, James and Torlak, Emina and Wang, Xi},
|
|
86 title = {Hyperkernel: Push-Button Verification of an OS Kernel},
|
|
87 booktitle = {Proceedings of the 26th Symposium on Operating Systems Principles},
|
|
88 series = {SOSP '17},
|
|
89 year = {2017},
|
|
90 isbn = {978-1-4503-5085-3},
|
|
91 location = {Shanghai, China},
|
|
92 pages = {252--269},
|
|
93 numpages = {18},
|
|
94 url = {http://doi.acm.org/10.1145/3132747.3132748},
|
|
95 doi = {10.1145/3132747.3132748},
|
|
96 acmid = {3132748},
|
|
97 publisher = {ACM},
|
|
98 address = {New York, NY, USA},
|
|
99 }
|
|
100
|
0
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
101 @inproceedings{Sigurbjarnarson:2016:PVF:3026877.3026879,
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
102 author = {Sigurbjarnarson, Helgi and Bornholt, James and Torlak, Emina and Wang, Xi},
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
103 title = {Push-button Verification of File Systems via Crash Refinement},
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
104 booktitle = {Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation},
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
105 series = {OSDI'16},
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
106 year = {2016},
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
107 isbn = {978-1-931971-33-1},
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
108 location = {Savannah, GA, USA},
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
109 pages = {1--16},
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
110 numpages = {16},
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
111 url = {http://dl.acm.org/citation.cfm?id=3026877.3026879},
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
112 acmid = {3026879},
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
113 publisher = {USENIX Association},
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
114 address = {Berkeley, CA, USA},
|
ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
115 }
|
13
|
116
|
|
117 @inproceedings{OSBook,
|
|
118 author = {Andrew S. Tanenbaum},
|
|
119 booktitle = {Modern Operating Systems Fourth Edition},
|
|
120 series = {OSDI'15},
|
|
121 year = {2015},
|
|
122 isbn = {978-0-13-359162-0},
|
|
123 location = {Hervert BOS Vrije Universiteit Amsterdam, The Netherlands},
|
|
124 pages = {265-332},
|
|
125 numpages = {67},
|
|
126 }
|
|
127
|
|
128
|
|
129 @misc{hg:cbcgcc,
|
|
130 title = {CbC\_gcc},
|
|
131 author = {並列信頼研究室},
|
|
132 organization = "琉球大学",
|
|
133 howpublished = {\url{http://www.cr.ie.u-ryukyu.ac.jp/hg/CbC/CbC_gcc/}},
|
|
134 note = {Accessed: 2021-01-31},
|
|
135 }
|
|
136
|
|
137 @misc{hg:gears,
|
|
138 title = {GearsOS},
|
|
139 author = {並列信頼研究室},
|
|
140 organization = "琉球大学",
|
|
141 howpublished = {\url{http://www.cr.ie.u-ryukyu.ac.jp/hg/Gears/Gears/}},
|
|
142 note = {Accessed: 2021-01-31},
|
|
143 }
|
|
144
|
|
145 @misc{hg:Christie,
|
|
146 title = {Christie},
|
|
147 author = {並列信頼研究室},
|
|
148 organization = "琉球大学",
|
|
149 howpublished = {\url{http://www.cr.ie.u-ryukyu.ac.jp/hg/Database/Christie/}},
|
|
150 note = {Accessed: 2021-01-31},
|
|
151 }
|
|
152
|
|
153
|
|
154 @article{
|
|
155 gears,
|
|
156 author = "河野 真治 and 伊波 立樹 and 東恩納 琢偉",
|
|
157 title = "Code Gear、Data Gear に基づく OS のプロトタイプ",
|
|
158 journal = "情報処理学会システムソフトウェアとオペレーティング・システム研究会(OS)",
|
|
159 month = "May",
|
|
160 year = 2016
|
|
161 }
|
|
162
|
|
163 @article{
|
|
164 anatofz,
|
|
165 author = "清水 隆博 and 河野真治",
|
|
166 title = "GearsOSのメタ計算",
|
|
167 journal = "琉球大学理工学研究科修士論文",
|
|
168 month = "Merch",
|
|
169 year = 2020
|
|
170 }
|
|
171
|
|
172 @article{
|
|
173 koki,
|
|
174 author = "宮城 光輝 and 河野真治",
|
|
175 title = "継続を基本とした言語による OS のモジュール化",
|
|
176 journal = "琉球大学理工学研究科修士論文",
|
|
177 month = "Merch",
|
|
178 year = 2018
|
|
179 }
|
|
180
|
|
181 @article{
|
|
182 tokumori,
|
|
183 author = "徳森 海斗 and 河野真治",
|
|
184 title = "LLVM Clang 上の Continuation based C コンパイラ の改良",
|
|
185 journal = "琉球大学理工学研究科修士論文",
|
|
186 month = "Merch",
|
|
187 year = 2016
|
|
188 }
|
|
189
|
|
190
|
|
191 @article{
|
|
192 mata-thesis,
|
|
193 author = "又吉 雄斗 and 河野 真治",
|
|
194 title = "GearsOS における inode を用いた File system の設計",
|
|
195 journal = "琉球大学工学部知能情報コース卒業論文",
|
|
196 month = "Merch",
|
|
197 year = 2022
|
|
198 }
|
|
199
|
|
200
|
|
201 @article{
|
|
202 pop,
|
|
203 author = "照屋 のぞみ and 河野 真治",
|
|
204 title = "分散フレームワークChristieの設計",
|
|
205 journal = "琉球大学理工学研究科修士論文",
|
|
206 month = "Merch",
|
|
207 year = 2018
|
|
208 }
|
|
209
|
|
210 @article{
|
|
211 Alice,
|
|
212 author = "赤嶺 一樹 and 河野 真治",
|
|
213 title = "分散ネットワークフレームワークAlice の 提案と実装",
|
|
214 journal = "琉球大学理工学研究科修士論文",
|
|
215 month = "Merch",
|
|
216 year = 2012
|
|
217 }
|
|
218
|
|
219 @article{
|
|
220 BlockChain,
|
|
221 author = "赤堀 貴一 and 河野 真治",
|
|
222 title = "Christieによるブロックチェーンの実装",
|
|
223 journal = "琉球大学工学部情報工学科卒業論文",
|
|
224 month = "Merch",
|
|
225 year = 2019
|
|
226 }
|
|
227
|
|
228 @manual{man:socket,
|
|
229 author = "{man-page of SOCKET}",
|
|
230 title ="{\url{https://linuxjm.osdn.jp/html/LDP_man-pages/man2/socket.2.html}}",
|
|
231 }
|
|
232
|
|
233 @manual{man:getaddrinfo,
|
|
234 author = "{man-page of GETADDRINFO}",
|
|
235 title ="{\url{https://linuxjm.osdn.jp/html/LDP_man-pages/man3/getaddrinfo.3.html}}",
|
|
236 }
|