1THIS FILE IS COPIED AND ADAPTED FROM GENERATED BIB FILE IN OUR PLDI'16 REPO 2,-------------------. 3| PREAMBLE | 4`-------------------' 5 6@preamble{ "\providecommand{\noopsort}[1]{} 7 \providecommand{\url}{\error{The bib files now require `url' 8 package!}}" 9} 10 11,-------------------. 12| BIBTEX ENTRIES | 13`-------------------' 14 15@misc{ASPLOS_16, 16 author = {Anonymous}, 17 note = {To Appear in ASPLOS'16. Copy available as anonymous 18 supplementary material for double blind review.}, 19 title = {\cogent: Verifying High-Assurance File System 20 Implementations}, 21 year = {2016}, 22} 23 24@inproceedings{Ahmed_FM_05, 25 author = {Amal Ahmed and Matthew Fluet and Greg Morrisett}, 26 booktitle = {10th ICFP}, 27 pages = {78--91}, 28 publisher = {ACM}, 29 title = {A Step-Indexed Model of Substructural State}, 30 year = {2005}, 31} 32 33@inproceedings{Barendsen_Smeters_93, 34 author = {Barendsen, Erik and Smetsers, Sjaak}, 35 booktitle = {FSTTCS}, 36 editor = {Shyamasundar, RudrapatnaK}, 37 pages = {41--51}, 38 publisher = {Springer}, 39 series = {LNCS}, 40 title = {Conventional and Uniqueness Typing in Graph Rewrite 41 Systems}, 42 volume = {761}, 43 year = {1993}, 44} 45 46@book{Bertot_Casteran:CoqArt, 47 author = {Yves Bertot and Pierre Cast{\'e}ran}, 48 publisher = {Springer}, 49 series = {Texts in Theoretical Computer Science. An EATCS 50 Series}, 51 title = {Interactive Theorem Proving and Program Development. 52 {Coq'Art}: The Calculus of Inductive Constructions}, 53 year = {2004}, 54 NOdoi = {10.1007/978-3-662-07964-5}, 55 NOisbn = {3-540-20854-2}, 56} 57 58@misc{Cogent_16, 59 author = {Anonymous}, 60 note = {Link to the repository removed for double blind 61 review, and is available from PLDI PC upon request.}, 62 title = {Companion Webpage: {\cogent} compiler, proofs, and file 63 systems}, 64 year = {2016}, 65} 66 67@article{Chargueraud_10, 68 address = {New York, NY, USA}, 69 author = {Arthur Chargu{\'e}raud}, 70 journal = {SIGPLAN Not.}, 71 month = {Sep}, 72 number = {9}, 73 pages = {321--332}, 74 publisher = {ACM}, 75 title = {Program Verification Through Characteristic Formulae}, 76 volume = {45}, 77 year = {2010}, 78 NOdoi = {10.1145/1932681.1863590}, 79 NOissn = {0362-1340}, 80 url = {http://doi.acm.org/10.1145/1932681.1863590}, 81} 82 83@article{Chargueraud_11, 84 address = {New York, NY, USA}, 85 author = {Arthur Chargu{\'e}raud}, 86 journal = {SIGPLAN Not.}, 87 month = {Sep}, 88 number = {9}, 89 pages = {418--430}, 90 publisher = {ACM}, 91 title = {Characteristic Formulae for the Verification of 92 Imperative Programs}, 93 volume = {46}, 94 year = {2011}, 95 NOdoi = {10.1145/2034574.2034828}, 96 NOissn = {0362-1340}, 97 url = {http://doi.acm.org/10.1145/2034574.2034828}, 98} 99 100@inproceedings{Chen_ZCCKZ_15, 101 address = {Monterey, CA}, 102 author = {Haogang Chen and Daniel Ziegler and Tej Chajed and 103 Adam Chlipala and M. Frans Kaashoek and 104 Nickolai Zeldovich}, 105 booktitle = {}, 106 month = {Oct}, 107 note = {to appear}, 108 title = {Using {Crash} {Hoare} Logic for Certifying the {FSCQ} 109 File System}, 110 year = {2015}, 111} 112 113@inproceedings{Cock_KS_08, 114 address = {Montreal, Canada}, 115 author = {Cock, David and Klein, Gerwin and Sewell, Thomas}, 116 booktitle = {21st TPHOLs}, 117 editor = {{Otmane Ait Mohamed, C��sar Mu��oz, So�����ne Tahar}}, 118 month = {Aug}, 119 pages = {167-182}, 120 publisher = {Springer}, 121 title = {Secure Microkernels, State Monads and Scalable 122 Refinement}, 123 year = {2008}, 124 NOdoi = {10.1007/978-3-540-71067-7_16}, 125} 126 127@book{Dijkstra_97, 128 address = {Upper Saddle River, NJ, USA}, 129 author = {Dijkstra, Edsger Wybe}, 130 edition = {1st}, 131 publisher = {Prentice Hall PTR}, 132 title = {A Discipline of Programming}, 133 year = {1997}, 134 NOisbn = {013215871X}, 135} 136 137@inproceedings{Ennals_SM_04, 138 author = {Rob Ennals and Richard Sharp and Alan Mycroft}, 139 booktitle = {13th ESOP}, 140 editor = {David Schmidt}, 141 pages = {204--218}, 142 publisher = {Springer}, 143 series = {LNCS}, 144 title = {Linear Types for Packet Processing}, 145 volume = {2986}, 146 year = {2004}, 147} 148 149@article{Fahndrich_DeLine_02, 150 address = {New York, NY, USA}, 151 author = {Manuel Fahndrich and Robert DeLine}, 152 journal = {SIGPLAN Not.}, 153 month = {May}, 154 number = {5}, 155 pages = {13--24}, 156 publisher = {ACM}, 157 title = {Adoption and Focus: Practical Linear Types for 158 Imperative Programming}, 159 volume = {37}, 160 year = {2002}, 161 NOdoi = {10.1145/543552.512532}, 162 NOissn = {0362-1340}, 163 url = {http://doi.acm.org/10.1145/543552.512532}, 164} 165 166@misc{Filebench:misc, 167 author = {Filebench developers}, 168 howpublished = {\url{http://sourceforge.net/projects/filebench}}, 169 key = {Filebench}, 170 title = {{Filebench} file system benchmark}, 171} 172 173@misc{Go:lang, 174 howpublished = {\url{https://go.googlesource.com/go}}, 175 key = {Go}, 176 note = {Accessed Nov 2015}, 177 title = {The {Go} Programming Language}, 178 year = {2015}, 179} 180 181@inproceedings{Greenaway_AK_12, 182 address = {Princeton, New Jersey, USA}, 183 author = {Greenaway, David and Andronick, June and 184 Klein, Gerwin}, 185 booktitle = {ITP}, 186 editor = {{Lennart Beringer and Amy Felty}}, 187 month = {Aug}, 188 pages = {99-115}, 189 publisher = {Springer Berlin / Heidelberg}, 190 title = {Bridging the Gap: Automatic Verified Abstraction of 191 {C}}, 192 year = {2012}, 193 NOdoi = {10.1007/978-3-642-32347-8_8}, 194} 195 196@inproceedings{Greenaway_LAK_14, 197 address = {Edinburgh, UK}, 198 author = {Greenaway, David and Lim, Japheth and Andronick, June and 199 Klein, Gerwin}, 200 booktitle = {PLDI}, 201 month = {Jun}, 202 pages = {429--439}, 203 publisher = {ACM}, 204 title = {Don't Sweat the Small Stuff: Formal Verification of 205 {C} Code Without the Pain}, 206 year = {2014}, 207 NOdoi = {10.1145/2594291.2594296}, 208} 209 210@techreport{Habit:lang, 211 address = {Portland, OR, USA}, 212 author = {{HASP project}}, 213 institution = {Department of Computer Science, Portland State 214 University}, 215 month = {Nov}, 216 number = {\url{http://hasp.cs.pdx.edu/habit-report-Nov2010.pdf}}, 217 title = {The {Habit} Programming Language: The Revised 218 Preliminary Report}, 219 year = {2010}, 220} 221 222@inproceedings{Hofmann_00, 223 author = {Martin Hofmann}, 224 booktitle = {ESOP}, 225 editor = {Smolka, Gert}, 226 pages = {165--179}, 227 publisher = {Springer}, 228 series = {LNCS}, 229 title = {A Type System for Bounded Space and Functional 230 In-Place Update--Extended Abstract.}, 231 volume = {1782}, 232 year = {2000}, 233} 234 235@inproceedings{Keller_MAOCRKH_13, 236 address = {Farmington, Pennsylvania, USA}, 237 author = {Keller, Gabi and Murray, Toby and Amani, Sidney and 238 O'Connor-Davis, Liam and Chen, Zilin and 239 Ryzhyk, Leonid and Klein, Gerwin and Heiser, Gernot}, 240 booktitle = {PLOS}, 241 month = {Nov}, 242 pages = {1-7}, 243 title = {File Systems Deserve Verification Too!}, 244 year = {2013}, 245 NOdoi = {10.1145/2525528.2525530}, 246} 247 248@inproceedings{Klein_EHACDEEKNSTW_09, 249 address = {Big Sky, MT, USA}, 250 author = {Klein, Gerwin and Elphinstone, Kevin and 251 Heiser, Gernot and Andronick, June and Cock, David and 252 Derrin, Philip and Elkaduwe, Dhammika and 253 Engelhardt, Kai and Kolanski, Rafal and 254 Norrish, Michael and Sewell, Thomas and Tuch, Harvey and 255 Winwood, Simon}, 256 booktitle = {SOSP}, 257 month = {Oct}, 258 pages = {207-220}, 259 publisher = {ACM}, 260 title = {{seL4}: Formal Verification of an {OS} Kernel}, 261 year = {2009}, 262} 263 264@article{Klein_AEMSKH_14, 265 author = {Klein, Gerwin and Andronick, June and 266 Elphinstone, Kevin and Murray, Toby and 267 Sewell, Thomas and Kolanski, Rafal and 268 Heiser, Gernot}, 269 journal = {Trans. Comp. Syst.}, 270 month = {Feb}, 271 number = {1}, 272 pages = {2:1-2:70}, 273 title = {Comprehensive Formal Verification of an {OS} 274 Microkernel}, 275 volume = {32}, 276 year = {2014}, 277 NOdoi = {10.1145/2560537}, 278} 279 280@inproceedings{Gu_KRSWWZG_15, 281 author = {Ronghui Gu and J{\'{e}}r{\'{e}}mie Koenig and 282 Tahina Ramananandro and Zhong Shao and 283 Xiongnan (Newman) Wu and Shu{-}Chun Weng and 284 Haozhong Zhang and Yu Guo}, 285 booktitle = {42nd POPL}, 286 editor = {Sriram K. Rajamani and David Walker}, 287 pages = {595--608}, 288 publisher = {{ACM}}, 289 title = {Deep Specifications and Certified Abstraction Layers}, 290 year = {2015}, 291 NOdoi = {10.1145/2676726.2676975}, 292} 293 294@inproceedings{Beringer_PYA_15, 295 author = {Lennart Beringer and Adam Petcher and Katherine Q. Ye and 296 Andrew W. Appel}, 297 booktitle = {24th USENIX Security}, 298 note = {To appear}, 299 publisher = {USENIX}, 300 title = {Verified correctness and security of {OpenSSL HMAC}}, 301 year = {2015}, 302} 303 304@inproceedings{Kumar_MNO_14, 305 address = {San Diego}, 306 author = {Kumar, Ramana and Myreen, Magnus and Norrish, Michael and 307 Owens, Scott}, 308 booktitle = {POPL}, 309 editor = {{Peter Sewell}}, 310 month = {Jan}, 311 pages = {179--191}, 312 publisher = {ACM Press}, 313 title = {{CakeML}: A Verified Implementation of {ML}}, 314 year = {2014}, 315 NOdoi = {10.1145/2535838.2535841}, 316} 317 318@inproceedings{Leroy_06, 319 address = {Charleston, SC, USA}, 320 author = {Xavier Leroy}, 321 booktitle = {33rd POPL}, 322 editor = {J. G. Morrisett and S. L. P. Jones}, 323 pages = {42--54}, 324 publisher = {ACM}, 325 title = {Formal certification of a compiler back-end, or: 326 Programming a compiler with a proof assistant}, 327 year = {2006}, 328} 329 330@article{Leroy_09, 331 author = {Xavier Leroy}, 332 journal = {CACM}, 333 number = {7}, 334 pages = {107--115}, 335 title = {Formal verification of a realistic compiler}, 336 volume = {52}, 337 year = {2009}, 338 NOdoi = {10.1145/1538788.1538814}, 339 NOissn = {0001-0782}, 340} 341 342@inproceedings{Mazurak_10, 343 address = {New York, NY, USA}, 344 author = {Mazurak, Karl and Zhao, Jianzhou and 345 Zdancewic, Steve}, 346 booktitle = {Proceedings of the 5th ACM SIGPLAN Workshop on Types 347 in Language Design and Implementation}, 348 pages = {77--88}, 349 publisher = {ACM}, 350 series = {TLDI '10}, 351 title = {{Lightweight Linear Types in System F${}^\circ$}}, 352 year = {2010}, 353 NOdoi = {10.1145/1708016.1708027}, 354 NOisbn = {978-1-60558-891-9}, 355 url = {http://doi.acm.org/10.1145/1708016.1708027}, 356} 357 358@inproceedings{McCreight_CT_10, 359 author = {McCreight, Andrew and Chevalier, Tim and 360 Tolmach, Andrew}, 361 booktitle = {15th ICFP}, 362 pages = {273--284}, 363 publisher = {ACM}, 364 title = {A Certified Framework for Compiling and Executing 365 Garbage-collected Languages}, 366 year = {2010}, 367} 368 369@misc{Mirabox:misc, 370 howpublished = 371 {\url{https://www.globalscaletechnologies.com/p-58-mirabox-development-kit.aspx}}, 372 key = {Mirabox}, 373 note = {Accessed Nov 2015}, 374 title = {{MiraBox} Development Kit}, 375 year = {2015}, 376} 377 378@book{Nipkow_Klein:Isabelle, 379 author = {Tobias Nipkow and Gerwin Klein}, 380 publisher = {Springer}, 381 title = {Concrete Semantics with {Isabelle/HOL}}, 382 year = {2014}, 383 NOdoi = {10.1007/978-3-319-10542-0}, 384 NOisbn = {978-3-319-10541-3}, 385} 386 387@inproceedings{Odersky_92, 388 author = {Martin Odersky}, 389 booktitle = {{ESOP} '92: 4th {E}uropean Symposium on Programming, 390 {R}ennes, France, Proceedings}, 391 editor = {B. Krieg-Br{\"{u}}ckner}, 392 month = {February}, 393 note = {Lecture Notes in Computer Science 582}, 394 pages = {390--407}, 395 publisher = {Springer-Verlag}, 396 title = {Observers for Linear Types}, 397 year = {1992}, 398} 399 400@book{Pierce_02, 401 author = {Benjamin C. Pierce}, 402 publisher = {MIT Press}, 403 title = {Types and Programming Languages}, 404 year = {2002}, 405} 406 407@inproceedings{Pike_HBEDL_14, 408 address = {San Diego, California, USA}, 409 author = {Pike, Lee and Hickey, Patrick and Bielman, James and 410 Elliott, Trevor and DuBuisson, Thomas and 411 Launchbury, John}, 412 booktitle = {2014PLPV}, 413 pages = {1--2}, 414 publisher = {ACM}, 415 title = {Programming Languages for High-assurance Autonomous 416 Vehicles: Extended Abstract}, 417 year = {2014}, 418 NOdoi = {10.1145/2541568.2541570}, 419} 420 421@misc{Rust:lang, 422 howpublished = {\url{http://rustlang.org}}, 423 key = {Rust}, 424 note = {Accessed March 2015}, 425 title = {The {Rust} Programming Language}, 426 year = {2014}, 427} 428 429@article{Sabry_Felleisen_92, 430 author = {Amr Sabry and Matthias Felleisen}, 431 journal = {SIGPLAN Lisp Pointers}, 432 month = {Jan}, 433 number = {1}, 434 pages = {288--298}, 435 publisher = {ACM}, 436 title = {Reasoning About Programs in Continuation-passing 437 Style}, 438 volume = {V}, 439 year = {1992}, 440} 441 442@inproceedings{Sewell_MK_13, 443 address = {Seattle, Washington, USA}, 444 author = {Sewell, Thomas and Myreen, Magnus and Klein, Gerwin}, 445 booktitle = {PLDI}, 446 month = {Jun}, 447 pages = {471-481}, 448 publisher = {ACM}, 449 title = {Translation Validation for a Verified {OS} Kernel}, 450 year = {2013}, 451} 452 453@inproceedings{Tuch_KN_07, 454 address = {Nice, France}, 455 author = {Tuch, Harvey and Klein, Gerwin and Norrish, Michael}, 456 booktitle = {POPL}, 457 editor = {{Martin Hofmann and Matthias Felleisen}}, 458 month = {Jan}, 459 pages = {97-108}, 460 publisher = {ACM}, 461 title = {Types, Bytes, and Separation Logic}, 462 year = {2007}, 463 NOisbn = {1-59593-575-4}, 464} 465 466@inproceedings{Wadler_90, 467 author = {Philip Wadler}, 468 booktitle = {Programming Concepts and Methods}, 469 title = {Linear types can change the world!}, 470 year = {1990}, 471} 472 473@misc{fstest:misc, 474 author = {Pawel Jakub Dawidek}, 475 howpublished = {\url{https://github.com/zfsonlinux/fstest}}, 476 key = {fstest}, 477 title = {{POSIX} file system test suite}, 478} 479 480@misc{greport, 481 author = {O'Connor-Davis, Liam}, 482 title = {{Definition of Core \cogent}}, 483 year = {2016}, 484} 485 486@phdthesis{schirmer:phd, 487 author = {Norbert Schirmer}, 488 school = {Technische Universit\"at M\"unchen}, 489 title = {Verification of Sequential Imperative Programs in 490 {I}sabelle/{HOL}}, 491 year = {2006}, 492} 493 494