{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:23:45Z","timestamp":1750220625500,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":28,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,10,27]],"date-time":"2019-10-27T00:00:00Z","timestamp":1572134400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["FA8750-16-C-0045"],"award-info":[{"award-number":["FA8750-16-C-0045"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2019,10,27]]},"DOI":"10.1145\/3365137.3365401","type":"proceedings-article","created":{"date-parts":[[2019,11,1]],"date-time":"2019-11-01T12:18:47Z","timestamp":1572610727000},"page":"67-73","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Trials and Tribulations in Synthesizing Operating Systems"],"prefix":"10.1145","author":[{"given":"Jingmei","family":"Hu","sequence":"first","affiliation":[{"name":"Harvard University, Cambridge, MA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Eric","family":"Lu","sequence":"additional","affiliation":[{"name":"Harvard University, Cambridge, MA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David A.","family":"Holland","sequence":"additional","affiliation":[{"name":"Harvard University, Cambridge, MA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ming","family":"Kawaguchi","sequence":"additional","affiliation":[{"name":"Harvard University, Cambridge, MA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stephen","family":"Chong","sequence":"additional","affiliation":[{"name":"Harvard University, Cambridge, MA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Margo I.","family":"Seltzer","sequence":"additional","affiliation":[{"name":"University of British Columbia, Vancouver, BC, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2019,10,27]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"5th International Conference on Learning Representations, ICLR 2017, Toulon, France, April 24-26, 2017, Conference Track Proceedings. https:\/\/openreview.net\/forum?id=ByldLrqlx","author":"Balog Matej","year":"2017","unstructured":"Matej Balog , Alexander L. Gaunt , Marc Brockschmidt , Sebastian Nowozin , and Daniel Tarlow . 2017 . DeepCoder: Learning to Write Programs . In 5th International Conference on Learning Representations, ICLR 2017, Toulon, France, April 24-26, 2017, Conference Track Proceedings. https:\/\/openreview.net\/forum?id=ByldLrqlx Matej Balog, Alexander L. Gaunt, Marc Brockschmidt, Sebastian Nowozin, and Daniel Tarlow. 2017. DeepCoder: Learning to Write Programs. In 5th International Conference on Learning Representations, ICLR 2017, Toulon, France, April 24-26, 2017, Conference Track Proceedings. https:\/\/openreview.net\/forum?id=ByldLrqlx"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629579"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706339"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062353"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00768-2_16"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192382"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2813885.2737977"},{"key":"e_1_3_2_1_9_1","volume-title":"Proceedings of the 12th USENIX conference on Operating Systems Design and Implementation (OSDI'16)","author":"Gu Ronghui","year":"2016","unstructured":"Ronghui Gu , Zhong Shao , Hao Chen , Xiongnan Wu , Jieung Kim , Vilhelm Sj\u00f6berg , and David Costanzo . 2016 . CertiKOS: an extensible architecture for building certified concurrent OS kernels . In Proceedings of the 12th USENIX conference on Operating Systems Design and Implementation (OSDI'16) . 653--669. Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan Wu, Jieung Kim, Vilhelm Sj\u00f6berg, and David Costanzo. 2016. CertiKOS: an extensible architecture for building certified concurrent OS kernels. In Proceedings of the 12th USENIX conference on Operating Systems Design and Implementation (OSDI'16). 653--669."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926423"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3282307"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISCAS.2001.922002"},{"volume-title":"Proceedings of the Second USENIX Symposium on Operating Systems Design and Implementation (OSDI '96)","author":"Mosberger David","key":"e_1_3_2_1_14_1","unstructured":"David Mosberger and Larry L. Peterson . 1996. Making Paths Explicit in the Scout Operating System . In Proceedings of the Second USENIX Symposium on Operating Systems Design and Implementation (OSDI '96) . ACM, New York, NY, USA, 153--167. https:\/\/doi.org\/10.1145\/238721.238771 10.1145\/238721.238771 David Mosberger and Larry L. Peterson. 1996. Making Paths Explicit in the Scout Operating System. In Proceedings of the Second USENIX Symposium on Operating Systems Design and Implementation (OSDI '96). ACM, New York, NY, USA, 153--167. https:\/\/doi.org\/10.1145\/238721.238771"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/357073.357079"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75293"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908093"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290385"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"crossref","unstructured":"Oleksandr Polozov and Sumit Gulwani. 2015. FlashMeta: A Framework for Inductive Program Synthesis. In OOPSLA 2015 Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming Systems Languages and Applications. 107--126.  Oleksandr Polozov and Sumit Gulwani. 2015. FlashMeta: A Framework for Inductive Program Synthesis. In OOPSLA 2015 Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming Systems Languages and Applications. 107--126.","DOI":"10.1145\/2814270.2814310"},{"key":"e_1_3_2_1_20_1","first-page":"11","article-title":"The Synthesis Kernel","volume":"1","author":"Pu Calton","year":"1988","unstructured":"Calton Pu , Henry Massalin , and John Ioannidis . 1988 . The Synthesis Kernel . Computing Systems 1 , 1 (1988), 11 -- 32 . Calton Pu, Henry Massalin, and John Ioannidis. 1988. The Synthesis Kernel. Computing Systems 1, 1 (1988), 11--32.","journal-title":"Computing Systems"},{"key":"e_1_3_2_1_21_1","volume-title":"Proceedings of 1986 ACM Fall Joint Computer Conference (ACM '86)","author":"Rashid Richard F.","year":"1986","unstructured":"Richard F. Rashid . 1986 . From RIG to Accent to Mach: The Evolution of a Network Operating System . In Proceedings of 1986 ACM Fall Joint Computer Conference (ACM '86) . IEEE Computer Society Press, Los Alamitos, CA, USA, 1128--1137. http:\/\/dl.acm.org\/citation.cfm?id=324493.325071 Richard F. Rashid. 1986. From RIG to Accent to Mach: The Evolution of a Network Operating System. In Proceedings of 1986 ACM Fall Joint Computer Conference (ACM '86). IEEE Computer Society Press, Los Alamitos, CA, USA, 1128--1137. http:\/\/dl.acm.org\/citation.cfm?id=324493.325071"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629583"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/2685048.2685101"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2080.2081"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375599"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1168857.1168907"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2006.02.003"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509578.2509586"},{"key":"e_1_3_2_1_29_1","volume-title":"Proceedings of the 2002 Design Automation Conference.","author":"Wolf Fabian","year":"2002","unstructured":"Fabian Wolf , Jan Staschulat , and Rolf Ernst . 2002 . Associative Caches in Formal Software Timing Analysis . In Proceedings of the 2002 Design Automation Conference. Fabian Wolf, Jan Staschulat, and Rolf Ernst. 2002. Associative Caches in Formal Software Timing Analysis. In Proceedings of the 2002 Design Automation Conference."}],"event":{"name":"SOSP '19: ACM SIGOPS 27th Symposium on Operating Systems Principles","sponsor":["SIGOPS ACM Special Interest Group on Operating Systems"],"location":"Huntsville ON Canada","acronym":"SOSP '19"},"container-title":["Proceedings of the 10th Workshop on Programming Languages and Operating Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3365137.3365401","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3365137.3365401","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3365137.3365401","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:01:30Z","timestamp":1750197690000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3365137.3365401"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,10,27]]},"references-count":28,"alternative-id":["10.1145\/3365137.3365401","10.1145\/3365137"],"URL":"https:\/\/doi.org\/10.1145\/3365137.3365401","relation":{},"subject":[],"published":{"date-parts":[[2019,10,27]]},"assertion":[{"value":"2019-10-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}