{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,16]],"date-time":"2026-01-16T03:37:57Z","timestamp":1768534677913,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":29,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,6,8]],"date-time":"2019-06-08T00:00:00Z","timestamp":1559952000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CNS-1563763,CCF-1836712"],"award-info":[{"award-number":["CNS-1563763,CCF-1836712"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100006785","name":"Google","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100006785","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2019,6,8]]},"DOI":"10.1145\/3314221.3314585","type":"proceedings-article","created":{"date-parts":[[2019,6,7]],"date-time":"2019-06-07T21:02:18Z","timestamp":1559941338000},"page":"1054-1068","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Argosy: verifying layered storage systems with recovery refinement"],"prefix":"10.1145","author":[{"given":"Tej","family":"Chajed","sequence":"first","affiliation":[{"name":"Massachusetts Institute of Technology, USA"}]},{"given":"Joseph","family":"Tassarotti","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, USA"}]},{"given":"M. Frans","family":"Kaashoek","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, USA"}]},{"given":"Nickolai","family":"Zeldovich","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, USA"}]}],"member":"320","published-online":{"date-parts":[[2019,6,8]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535862"},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679680900728X"},{"key":"e_1_3_2_2_3_1","unstructured":"Ryan Beckett Eric Campbell and Michael Greenberg. 2017. Kleene Algebra Modulo Theories. arXiv: cs.PL\/1707.02894  Ryan Beckett Eric Campbell and Michael Greenberg. 2017. Kleene Algebra Modulo Theories. arXiv: cs.PL\/1707.02894"},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908108"},{"key":"e_1_3_2_2_5_1","volume-title":"Deciding Kleene Algebras in Coq. Logical Methods in Computer Science 8, 1","author":"Braibant Thomas","year":"2012","unstructured":"Thomas Braibant and Damien Pous . 2012. Deciding Kleene Algebras in Coq. Logical Methods in Computer Science 8, 1 ( 2012 ). Thomas Braibant and Damien Pous. 2012. Deciding Kleene Algebras in Coq. Logical Methods in Computer Science 8, 1 (2012)."},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132776"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815402"},{"key":"e_1_3_2_2_9_1","unstructured":"Ernie Cohen. 1994. Lazy Caching in Kleene Algebra.  Ernie Cohen. 1994. Lazy Caching in Kleene Algebra."},{"key":"e_1_3_2_2_10_1","volume-title":"A Verified POSIX-Compliant Flash File System -Modular Verification Technology &amp","author":"Ernst Gidon","unstructured":"Gidon Ernst . 2016. A Verified POSIX-Compliant Flash File System -Modular Verification Technology &amp ; Crash Tolerance. Ph.D. Dissertation. Augsburg University . Gidon Ernst. 2016. A Verified POSIX-Compliant Flash File System -Modular Verification Technology & Crash Tolerance. Ph.D. Dissertation. Augsburg University."},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2016.04.009"},{"key":"e_1_3_2_2_12_1","volume-title":"ESOP 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings. 282\u2013309","author":"Foster Nate","year":"2016","unstructured":"Nate Foster , Dexter Kozen , Konstantinos Mamouras , Mark Reitblatt , and Alexandra Silva . 2016 . Probabilistic NetKAT. In Programming Languages and Systems - 25th European Symposium on Programming , ESOP 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings. 282\u2013309 . Nate Foster, Dexter Kozen, Konstantinos Mamouras, Mark Reitblatt, and Alexandra Silva. 2016. Probabilistic NetKAT. In Programming Languages and Systems - 25th European Symposium on Programming, ESOP 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings. 282\u2013309."},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/1812941.1812945"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192381"},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815428"},{"key":"e_1_3_2_2_16_1","unstructured":"Jan Kara. 2012. jbd2: issue cache flush after checkpointing even with internal journal. http:\/\/git.kernel.org\/ cgit\/linux\/kernel\/git\/stable\/linux-stable.git\/commit\/?id= 79feb521a44705262d15cc819a4117a447b11ea7 .  Jan Kara. 2012. jbd2: issue cache flush after checkpointing even with internal journal. http:\/\/git.kernel.org\/ cgit\/linux\/kernel\/git\/stable\/linux-stable.git\/commit\/?id= 79feb521a44705262d15cc819a4117a447b11ea7 ."},{"key":"e_1_3_2_2_17_1","unstructured":"Jan Kara. 2014. {PATCH} ext4: Forbid journal_async_commit in data=ordered mode. http:\/\/permalink.gmane.org\/gmane.comp. file-systems.ext4\/46977 .  Jan Kara. 2014. {PATCH} ext4: Forbid journal_async_commit in data=ordered mode. http:\/\/permalink.gmane.org\/gmane.comp. file-systems.ext4\/46977 ."},{"key":"e_1_3_2_2_18_1","volume-title":"MFCS (Lecture Notes in Computer Science)","author":"Kozen Dexter","unstructured":"Dexter Kozen . 1990. On Kleene Algebras and Closed Semirings . In MFCS (Lecture Notes in Computer Science) , Vol. 452 . Springer , 26\u201347. Dexter Kozen. 1990. On Kleene Algebras and Closed Semirings. In MFCS (Lecture Notes in Computer Science), Vol. 452. Springer, 26\u201347."},{"key":"e_1_3_2_2_20_1","volume-title":"First International Conference","author":"Kozen Dexter","year":"2000","unstructured":"Dexter Kozen and Maria-Christina Patron . 2000 . Certification of Compiler Optimizations Using Kleene Algebra with Tests. In Computational Logic - CL 2000 , First International Conference , London, UK , 24-28 July, 2000, Proceedings. 568\u2013582. Dexter Kozen and Maria-Christina Patron. 2000. Certification of Compiler Optimizations Using Kleene Algebra with Tests. In Computational Logic - CL 2000, First International Conference, London, UK, 24-28 July, 2000, Proceedings. 568\u2013582."},{"key":"e_1_3_2_2_21_1","volume-title":"Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers","author":"Lamport Leslie","year":"2002","unstructured":"Leslie Lamport . 2002 . Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers . Addison-Wesley . Leslie Lamport. 2002. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley."},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103711"},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/2591272.2591276"},{"key":"e_1_3_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1134"},{"key":"e_1_3_2_2_25_1","unstructured":"Nancy A. Lynch. 1996. Distributed Algorithms. Morgan Kaufmann.   Nancy A. Lynch. 1996. Distributed Algorithms. Morgan Kaufmann."},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-26529-2_10"},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39634-2_15"},{"key":"e_1_3_2_2_28_1","volume-title":"Proceedings of the 12th Symposium on Operating Systems Design and Implementation (OSDI)","author":"Sigurbjarnarson Helgi","year":"2016","unstructured":"Helgi Sigurbjarnarson , James Bornholt , Emina Torlak , and Xi Wang . 2016 . Push-Button Verification of File Systems via Crash Refinement . In Proceedings of the 12th Symposium on Operating Systems Design and Implementation (OSDI) . Savannah, GA. Helgi Sigurbjarnarson, James Bornholt, Emina Torlak, and Xi Wang. 2016. Push-Button Verification of File Systems via Crash Refinement. In Proceedings of the 12th Symposium on Operating Systems Design and Implementation (OSDI). Savannah, GA."},{"key":"e_1_3_2_2_29_1","unstructured":"The Coq Development Team. 2019. The Coq Proof Assistant version 8.9.0.  The Coq Development Team. 2019. The Coq Proof Assistant version 8.9.0."},{"key":"e_1_3_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2003.09.002"},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737958"}],"event":{"name":"PLDI '19: 40th ACM SIGPLAN Conference on Programming Language Design and Implementation","location":"Phoenix AZ USA","acronym":"PLDI '19","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3314221.3314585","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3314221.3314585","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3314221.3314585","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:53:22Z","timestamp":1750204402000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3314221.3314585"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,6,8]]},"references-count":29,"alternative-id":["10.1145\/3314221.3314585","10.1145\/3314221"],"URL":"https:\/\/doi.org\/10.1145\/3314221.3314585","relation":{},"subject":[],"published":{"date-parts":[[2019,6,8]]},"assertion":[{"value":"2019-06-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}