{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,6]],"date-time":"2026-05-06T23:05:37Z","timestamp":1778108737466,"version":"3.51.4"},"publisher-location":"New York, NY, USA","reference-count":58,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,10,23]],"date-time":"2023-10-23T00:00:00Z","timestamp":1698019200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100012166","name":"National Key Research and Development Program of China","doi-asserted-by":"publisher","award":["2022YFB4500700"],"award-info":[{"award-number":["2022YFB4500700"]}],"id":[{"id":"10.13039\/501100012166","id-type":"DOI","asserted-by":"publisher"}]},{"name":"National Natural Science Foundation of China under the grant number","award":["62172008"],"award-info":[{"award-number":["62172008"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2023,10,23]]},"DOI":"10.1145\/3600006.3613153","type":"proceedings-article","created":{"date-parts":[[2023,10,3]],"date-time":"2023-10-03T14:44:17Z","timestamp":1696344257000},"page":"80-95","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Automated Verification of an In-Production DNS Authoritative Engine"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2231-7901","authenticated-orcid":false,"given":"Naiqian","family":"Zheng","sequence":"first","affiliation":[{"name":"Peking University, Beijing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7027-4566","authenticated-orcid":false,"given":"Mengqi","family":"Liu","sequence":"additional","affiliation":[{"name":"Alibaba Cloud, Hangzhou, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-1942-9902","authenticated-orcid":false,"given":"Yuxing","family":"Xiang","sequence":"additional","affiliation":[{"name":"Peking University, Beijing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-9288-4778","authenticated-orcid":false,"given":"Linjian","family":"Song","sequence":"additional","affiliation":[{"name":"Alibaba Cloud, Hangzhou, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-7981-2468","authenticated-orcid":false,"given":"Dong","family":"Li","sequence":"additional","affiliation":[{"name":"Alibaba Cloud, Hangzhou, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-4816-5224","authenticated-orcid":false,"given":"Feng","family":"Han","sequence":"additional","affiliation":[{"name":"Alibaba Cloud, Hangzhou, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-3014-348X","authenticated-orcid":false,"given":"Nan","family":"Wang","sequence":"additional","affiliation":[{"name":"Alibaba Cloud, Hangzhou, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-4238-4695","authenticated-orcid":false,"given":"Yong","family":"Ma","sequence":"additional","affiliation":[{"name":"Alibaba Cloud, Hangzhou, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-3875-7902","authenticated-orcid":false,"given":"Zhuo","family":"Liang","sequence":"additional","affiliation":[{"name":"Alibaba Cloud, Hangzhou, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-5824-8911","authenticated-orcid":false,"given":"Dennis","family":"Cai","sequence":"additional","affiliation":[{"name":"Alibaba Cloud, San Jose, United States of America"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4352-7497","authenticated-orcid":false,"given":"Ennan","family":"Zhai","sequence":"additional","affiliation":[{"name":"Alibaba Cloud, Hangzhou, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7908-8484","authenticated-orcid":false,"given":"Xuanzhe","family":"Liu","sequence":"additional","affiliation":[{"name":"Peking University, Beijing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8741-5847","authenticated-orcid":false,"given":"Xin","family":"Jin","sequence":"additional","affiliation":[{"name":"Peking University, Beijing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,10,23]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"2017. How and why the leap second affected Cloudflare DNS. https:\/\/blog.cloudflare.com\/how-and-why-the-leap-second-affected-cloudflare-dns\/.  2017. How and why the leap second affected Cloudflare DNS. https:\/\/blog.cloudflare.com\/how-and-why-the-leap-second-affected-cloudflare-dns\/."},{"key":"e_1_3_2_1_2_1","unstructured":"2018. Analyzing the Impact of a Public DNS Resolver Outage. https:\/\/www.catchpoint.com\/blog\/google-dns-outage.  2018. Analyzing the Impact of a Public DNS Resolver Outage. https:\/\/www.catchpoint.com\/blog\/google-dns-outage."},{"key":"e_1_3_2_1_3_1","unstructured":"2021. A DNS outage just took down a large chunk of the internet. https:\/\/techcrunch.com\/2021\/07\/22\/a-dns-outage-just-took-down-a-good-chunk-of-the-internet\/.  2021. A DNS outage just took down a large chunk of the internet. https:\/\/techcrunch.com\/2021\/07\/22\/a-dns-outage-just-took-down-a-good-chunk-of-the-internet\/."},{"key":"e_1_3_2_1_4_1","unstructured":"2021. Observations on resolver behavior during DNS outages. https:\/\/blog.verisign.com\/security\/facebook-dns-outage\/.  2021. Observations on resolver behavior during DNS outages. https:\/\/blog.verisign.com\/security\/facebook-dns-outage\/."},{"key":"e_1_3_2_1_5_1","unstructured":"2021. Understanding how Facebook disappeared from the Internet. https:\/\/blog.cloudflare.com\/october-2021-facebook-outage\/.  2021. Understanding how Facebook disappeared from the Internet. https:\/\/blog.cloudflare.com\/october-2021-facebook-outage\/."},{"key":"e_1_3_2_1_6_1","unstructured":"2022. The Coq Proof Assistant. https:\/\/coq.inria.fr\/.  2022. The Coq Proof Assistant. https:\/\/coq.inria.fr\/."},{"key":"e_1_3_2_1_7_1","unstructured":"2022. Gollvm: LLVM-based Go compiler. https:\/\/go.googlesource.com\/gollvm.  2022. Gollvm: LLVM-based Go compiler. https:\/\/go.googlesource.com\/gollvm."},{"key":"e_1_3_2_1_8_1","unstructured":"Anish Athalye M Frans Kaashoek and Nickolai Zeldovich. 2022. Verifying Hardware Security Modules with {Information-Preserving} Refinement. In USENIX OSDI.  Anish Athalye M Frans Kaashoek and Nickolai Zeldovich. 2022. Verifying Hardware Security Modules with {Information-Preserving} Refinement. In USENIX OSDI."},{"key":"e_1_3_2_1_9_1","volume-title":"Jacob Van Geffen, and Andrew Warfield","author":"Bornholt James","year":"2021","unstructured":"James Bornholt , Rajeev Joshi , Vytautas Astrauskas , Brendan Cully , Bernhard Kragl , Seth Markle , Kyle Sauri , Drew Schleit , Grant Slatton , Serdar Tasiran , Jacob Van Geffen, and Andrew Warfield . 2021 . Using lightweight formal methods to validate a key-value storage node in Amazon S3. In ACM SOSP. James Bornholt, Rajeev Joshi, Vytautas Astrauskas, Brendan Cully, Bernhard Kragl, Seth Markle, Kyle Sauri, Drew Schleit, Grant Slatton, Serdar Tasiran, Jacob Van Geffen, and Andrew Warfield. 2021. Using lightweight formal methods to validate a key-value storage node in Amazon S3. In ACM SOSP."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276519"},{"key":"e_1_3_2_1_11_1","volume-title":"IRONSIDES: DNS with no singlepacket denial of service or remote code execution vulnerabilities","author":"Carlisle Martin","year":"2012","unstructured":"Martin Carlisle and Barry Fagin . 2012 . IRONSIDES: DNS with no singlepacket denial of service or remote code execution vulnerabilities . In IEEE GLOBECOM. Martin Carlisle and Barry Fagin. 2012. IRONSIDES: DNS with no singlepacket denial of service or remote code execution vulnerabilities. In IEEE GLOBECOM."},{"key":"e_1_3_2_1_12_1","unstructured":"Tej Chajed Joseph Tassarotti Mark Theng M Frans Kaashoek and Nickolai Zeldovich. 2022. Verifying the {DaisyNFS} concurrent and crash-safe file system with sequential reasoning. In USENIX OSDI.  Tej Chajed Joseph Tassarotti Mark Theng M Frans Kaashoek and Nickolai Zeldovich. 2022. Verifying the {DaisyNFS} concurrent and crash-safe file system with sequential reasoning. In USENIX OSDI."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"crossref","unstructured":"Haogang Chen Tej Chajed Alex Konradi Stephanie Wang Atalay \u0130leri Adam Chlipala M Frans Kaashoek and Nickolai Zeldovich. 2017. Verifying a high-performance crash-safe file system using a tree specification. In ACM SOSP.  Haogang Chen Tej Chajed Alex Konradi Stephanie Wang Atalay \u0130leri Adam Chlipala M Frans Kaashoek and Nickolai Zeldovich. 2017. Verifying a high-performance crash-safe file system using a tree specification. In ACM SOSP.","DOI":"10.1145\/3132747.3132776"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"crossref","unstructured":"Hao Chen Xiongnan Wu Zhong Shao Joshua Lockerman and Ronghui Gu. 2016. Toward compositional verification of interruptible OS kernels and device drivers. In ACM PLDI.  Hao Chen Xiongnan Wu Zhong Shao Joshua Lockerman and Ronghui Gu. 2016. Toward compositional verification of interruptible OS kernels and device drivers. In ACM PLDI.","DOI":"10.1145\/2908080.2908101"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"crossref","unstructured":"Haogang Chen Daniel Ziegler Tej Chajed Adam Chlipala M Frans Kaashoek and Nickolai Zeldovich. 2015. Using Crash Hoare logic for certifying the FSCQ file system. In ACM SOSP.  Haogang Chen Daniel Ziegler Tej Chajed Adam Chlipala M Frans Kaashoek and Nickolai Zeldovich. 2015. Using Crash Hoare logic for certifying the FSCQ file system. In ACM SOSP.","DOI":"10.1145\/2815400.2815402"},{"key":"e_1_3_2_1_16_1","volume-title":"End-to-end verification of information-flow security for C and assembly programs. ACM SIGPLAN Notices","author":"Costanzo David","year":"2016","unstructured":"David Costanzo , Zhong Shao , and Ronghui Gu. 2016. End-to-end verification of information-flow security for C and assembly programs. ACM SIGPLAN Notices ( 2016 ). David Costanzo, Zhong Shao, and Ronghui Gu. 2016. End-to-end verification of information-flow security for C and assembly programs. ACM SIGPLAN Notices (2016)."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"crossref","unstructured":"Mihai Dobrescu and Katerina Argyraki. 2014. Software Dataplane Verification. In USENIX NSDI.  Mihai Dobrescu and Katerina Argyraki. 2014. Software Dataplane Verification. In USENIX NSDI.","DOI":"10.1145\/2823400"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"crossref","unstructured":"R. Elz. 1997. Clarifications to the DNS Specification. RFC 2181. https:\/\/www.rfc-editor.org\/info\/rfc2181  R. Elz. 1997. Clarifications to the DNS Specification. RFC 2181. https:\/\/www.rfc-editor.org\/info\/rfc2181","DOI":"10.17487\/rfc2181"},{"key":"e_1_3_2_1_20_1","unstructured":"Ronghui Gu J\u00e9r\u00e9mie Koenig Tahina Ramananandro Zhong Shao Xiongnan (Newman) Wu Shu-Chun Weng Haozhong Zhang and Yu Guo. 2015. Deep Specifications and Certified Abstraction Layers. In ACM POPL.  Ronghui Gu J\u00e9r\u00e9mie Koenig Tahina Ramananandro Zhong Shao Xiongnan (Newman) Wu Shu-Chun Weng Haozhong Zhang and Yu Guo. 2015. Deep Specifications and Certified Abstraction Layers. In ACM POPL."},{"key":"e_1_3_2_1_21_1","unstructured":"Ronghui Gu Zhong Shao Hao Chen Xiongnan (Newman) Wu Jieung Kim Vilhelm Sj\u00f6berg and David Costanzo. 2016. CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels.. In USENIX OSDI.  Ronghui Gu Zhong Shao Hao Chen Xiongnan (Newman) Wu Jieung Kim Vilhelm Sj\u00f6berg and David Costanzo. 2016. CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels.. In USENIX OSDI."},{"key":"e_1_3_2_1_22_1","volume-title":"Certified concurrent abstraction layers. ACM SIGPLAN Notices","author":"Gu Ronghui","year":"2018","unstructured":"Ronghui Gu , Zhong Shao , Jieung Kim , Xiongnan Wu , J\u00e9r\u00e9mie Koenig , Vilhelm Sj\u00f6berg , Hao Chen , David Costanzo , and Tahina Ramananandro . 2018. Certified concurrent abstraction layers. ACM SIGPLAN Notices ( 2018 ). Ronghui Gu, Zhong Shao, Jieung Kim, Xiongnan Wu, J\u00e9r\u00e9mie Koenig, Vilhelm Sj\u00f6berg, Hao Chen, David Costanzo, and Tahina Ramananandro. 2018. Certified concurrent abstraction layers. ACM SIGPLAN Notices (2018)."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25543-5_28"},{"key":"e_1_3_2_1_24_1","volume-title":"Groot: Proactive verification of dns configurations. In ACM SIGCOMM.","author":"Reddy Kakarla Siva Kesava","year":"2020","unstructured":"Siva Kesava Reddy Kakarla , Ryan Beckett , Behnaz Arzani , Todd Millstein , and George Varghese . 2020 . Groot: Proactive verification of dns configurations. In ACM SIGCOMM. Siva Kesava Reddy Kakarla, Ryan Beckett, Behnaz Arzani, Todd Millstein, and George Varghese. 2020. Groot: Proactive verification of dns configurations. In ACM SIGCOMM."},{"key":"e_1_3_2_1_25_1","unstructured":"Siva Kesava Reddy Kakarla Ryan Beckett Todd Millstein and George Varghese. 2022. {SCALE}: Automatically Finding {RFC} Compliance Bugs in {DNS} Nameservers. In USENIX NSDI.  Siva Kesava Reddy Kakarla Ryan Beckett Todd Millstein and George Varghese. 2022. {SCALE}: Automatically Finding {RFC} Compliance Bugs in {DNS} Nameservers. In USENIX NSDI."},{"key":"e_1_3_2_1_26_1","volume-title":"Symbolic execution and program testing. Commun. ACM","author":"King James C","year":"1976","unstructured":"James C King . 1976. Symbolic execution and program testing. Commun. ACM ( 1976 ). James C King. 1976. Symbolic execution and program testing. Commun. ACM (1976)."},{"key":"e_1_3_2_1_27_1","volume-title":"Comprehensive formal verification of an OS microkernel. ACM Transactions on Computer Systems","author":"Klein Gerwin","year":"2014","unstructured":"Gerwin Klein , June Andronick , Kevin Elphinstone , Toby Murray , Thomas Sewell , Rafal Kolanski , and Gernot Heiser . 2014. Comprehensive formal verification of an OS microkernel. ACM Transactions on Computer Systems ( 2014 ). Gerwin Klein, June Andronick, Kevin Elphinstone, Toby Murray, Thomas Sewell, Rafal Kolanski, and Gernot Heiser. 2014. Comprehensive formal verification of an OS microkernel. ACM Transactions on Computer Systems (2014)."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"crossref","unstructured":"Gerwin Klein Kevin Elphinstone Gernot Heiser June Andronick David Cock Philip Derrin Dhammika Elkaduwe Kai Engelhardt Rafal Kolanski Michael Norrish etal 2009. seL4: Formal verification of an OS kernel. In ACM SOSP.  Gerwin Klein Kevin Elphinstone Gernot Heiser June Andronick David Cock Philip Derrin Dhammika Elkaduwe Kai Engelhardt Rafal Kolanski Michael Norrish et al. 2009. seL4: Formal verification of an OS kernel. In ACM SOSP.","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/CGO.2004.1281665"},{"key":"e_1_3_2_1_30_1","volume-title":"Formal verification of a realistic compiler. Commun. ACM","author":"Leroy Xavier","year":"2009","unstructured":"Xavier Leroy . 2009. Formal verification of a realistic compiler. Commun. ACM ( 2009 ). Xavier Leroy. 2009. Formal verification of a realistic compiler. Commun. ACM (2009)."},{"key":"e_1_3_2_1_31_1","unstructured":"E. Lewis. 1997. The Role of Wildcards in the Domain Name System. RFC 4592. https:\/\/www.rfc-editor.org\/info\/rfc4592  E. Lewis. 1997. The Role of Wildcards in the Domain Name System. RFC 4592. https:\/\/www.rfc-editor.org\/info\/rfc4592"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00049"},{"key":"e_1_3_2_1_33_1","unstructured":"Xupeng Li Xuheng Li Christoffer Dall Ronghui Gu Jason Nieh Yousuf Sait and Gareth Stockwell. 2022. Design and Verification of the Arm Confidential Compute Architecture. In USENIX OSDI.  Xupeng Li Xuheng Li Christoffer Dall Ronghui Gu Jason Nieh Yousuf Sait and Gareth Stockwell. 2022. Design and Verification of the Arm Confidential Compute Architecture. In USENIX OSDI."},{"key":"e_1_3_2_1_34_1","volume-title":"Virtual timeline: a formal abstraction for verifying preemptive schedulers with temporal isolation. ACM POPL","author":"Liu Mengqi","year":"2019","unstructured":"Mengqi Liu , Lionel Rieg , Zhong Shao , Ronghui Gu , David Costanzo , Jung-Eun Kim , and Man-Ki Yoon . 2019. Virtual timeline: a formal abstraction for verifying preemptive schedulers with temporal isolation. ACM POPL ( 2019 ). Mengqi Liu, Lionel Rieg, Zhong Shao, Ronghui Gu, David Costanzo, Jung-Eun Kim, and Man-Ki Yoon. 2019. Virtual timeline: a formal abstraction for verifying preemptive schedulers with temporal isolation. ACM POPL (2019)."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563290"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"crossref","unstructured":"Paul Mockapetris. 1987. Domain names-concepts and facilities. RFC 1034. https:\/\/www.rfc-editor.org\/rfc\/rfc1034  Paul Mockapetris. 1987. Domain names-concepts and facilities. RFC 1034. https:\/\/www.rfc-editor.org\/rfc\/rfc1034","DOI":"10.17487\/rfc1034"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"crossref","unstructured":"Paul V Mockapetris. 1987. Domain names-implementation and specification. https:\/\/www.rfc-editor.org\/rfc\/rfc1035  Paul V Mockapetris. 1987. Domain names-implementation and specification. https:\/\/www.rfc-editor.org\/rfc\/rfc1035","DOI":"10.17487\/rfc1035"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2013.35"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"crossref","unstructured":"Luke Nelson James Bornholt Ronghui Gu Andrew Baumann Emina Torlak and Xi Wang. 2019. Scaling symbolic evaluation for automated verification of systems code with Serval. In ACM SOSP.  Luke Nelson James Bornholt Ronghui Gu Andrew Baumann Emina Torlak and Xi Wang. 2019. Scaling symbolic evaluation for automated verification of systems code with Serval. In ACM SOSP.","DOI":"10.1145\/3341301.3359641"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132748"},{"key":"e_1_3_2_1_41_1","volume-title":"Emina Torlak, and Xi Wang.","author":"Nelson Luke","year":"2020","unstructured":"Luke Nelson , Jacob Van Geffen , Emina Torlak, and Xi Wang. 2020 . Specification and verification in the field: Applying formal methods to BPF just-in-time compilers in the Linux kernel. In USENIX OSDI. Luke Nelson, Jacob Van Geffen, Emina Torlak, and Xi Wang. 2020. Specification and verification in the field: Applying formal methods to BPF just-in-time compilers in the Linux kernel. In USENIX OSDI."},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"crossref","unstructured":"Tobias Nipkow Markus Wenzel and Lawrence C Paulson. 2002. Isabelle\/HOL: a proof assistant for higher-order logic.  Tobias Nipkow Markus Wenzel and Lawrence C Paulson. 2002. Isabelle\/HOL: a proof assistant for higher-order logic.","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_3_2_1_43_1","unstructured":"NMap. 2023. NMap DNS Fuzzing. https:\/\/nmap.org\/nsedoc\/scripts\/dns-fuzz.html  NMap. 2023. NMap DNS Fuzzing. https:\/\/nmap.org\/nsedoc\/scripts\/dns-fuzz.html"},{"key":"e_1_3_2_1_44_1","volume-title":"Diogo Behrens, Ming Fu, Antonio Paolillo, Lilith Oberhauser, Koustubha Bhat, Yuzhong Wen, Haibo Chen, Jaeho Kim, et al.","author":"Oberhauser Jonas","year":"2021","unstructured":"Jonas Oberhauser , Rafael Lourenco de Lima Chehab , Diogo Behrens, Ming Fu, Antonio Paolillo, Lilith Oberhauser, Koustubha Bhat, Yuzhong Wen, Haibo Chen, Jaeho Kim, et al. 2021 . VSync: pushbutton verification and optimization for synchronization primitives on weak memory models. In ACM ASPLOS. Jonas Oberhauser, Rafael Lourenco de Lima Chehab, Diogo Behrens, Ming Fu, Antonio Paolillo, Lilith Oberhauser, Koustubha Bhat, Yuzhong Wen, Haibo Chen, Jaeho Kim, et al. 2021. VSync: pushbutton verification and optimization for synchronization primitives on weak memory models. In ACM ASPLOS."},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"crossref","unstructured":"Oded Padon Kenneth L McMillan Aurojit Panda Mooly Sagiv and Sharon Shoham. 2016. Ivy: safety verification by interactive generalization. In ACM PLDI.  Oded Padon Kenneth L McMillan Aurojit Panda Mooly Sagiv and Sharon Shoham. 2016. Ivy: safety verification by interactive generalization. In ACM PLDI.","DOI":"10.1145\/2908080.2908118"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3102980.3102986"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTAS.2016.7461326"},{"key":"e_1_3_2_1_48_1","unstructured":"Thomas Arthur Leck Sewell Magnus O Myreen and Gerwin Klein. 2013. Translation validation for a verified OS kernel. In ACM PLDI.  Thomas Arthur Leck Sewell Magnus O Myreen and Gerwin Klein. 2013. Translation validation for a verified OS kernel. In ACM PLDI."},{"key":"e_1_3_2_1_49_1","volume-title":"Nickel: A framework for design and verification of information flow control systems. In USENIX OSDI.","author":"Sigurbjarnarson Helgi","year":"2018","unstructured":"Helgi Sigurbjarnarson , Luke Nelson , Bruno Castro-Karney , James Bornholt , Emina Torlak , and Xi Wang . 2018 . Nickel: A framework for design and verification of information flow control systems. In USENIX OSDI. Helgi Sigurbjarnarson, Luke Nelson, Bruno Castro-Karney, James Bornholt, Emina Torlak, and Xi Wang. 2018. Nickel: A framework for design and verification of information flow control systems. In USENIX OSDI."},{"key":"e_1_3_2_1_50_1","unstructured":"Robert Swiecki and Anestis Bechtsoudis. 2020. Google Honggfuzz DNS Fuzzing. https:\/\/github.com\/google\/honggfuzz\/tree\/master\/examples\/bind  Robert Swiecki and Anestis Bechtsoudis. 2020. Google Honggfuzz DNS Fuzzing. https:\/\/github.com\/google\/honggfuzz\/tree\/master\/examples\/bind"},{"key":"e_1_3_2_1_51_1","unstructured":"Runzhou Tao Jianan Yao Xupeng Li Shih-Wei Li Jason Nieh and Ronghui Gu. 2021. Formal verification of a multiprocessor hypervisor on arm relaxed memory hardware. In ACM SOSP.  Runzhou Tao Jianan Yao Xupeng Li Shih-Wei Li Jason Nieh and Ronghui Gu. 2021. Formal verification of a multiprocessor hypervisor on arm relaxed memory hardware. In ACM SOSP."},{"key":"e_1_3_2_1_52_1","unstructured":"Runzhou Tao Jianan Yao Xupeng Li Shih-Wei Li Jason Nieh and Ronghui Gu. 2021. Formal verification of a multiprocessor hypervisor on arm relaxed memory hardware. In ACM SOSP.  Runzhou Tao Jianan Yao Xupeng Li Shih-Wei Li Jason Nieh and Ronghui Gu. 2021. Formal verification of a multiprocessor hypervisor on arm relaxed memory hardware. In ACM SOSP."},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509578.2509586"},{"key":"e_1_3_2_1_54_1","volume-title":"A lightweight symbolic virtual machine for solver-aided host languages. ACM SIGPLAN Notices","author":"Torlak Emina","year":"2014","unstructured":"Emina Torlak and Rastislav Bodik . 2014. A lightweight symbolic virtual machine for solver-aided host languages. ACM SIGPLAN Notices ( 2014 ). Emina Torlak and Rastislav Bodik. 2014. A lightweight symbolic virtual machine for solver-aided host languages. ACM SIGPLAN Notices (2014)."},{"key":"e_1_3_2_1_55_1","unstructured":"P. Vixie. 1997. Dynamic Updates in the Domain Name System (DNS UPDATE). RFC 2136. https:\/\/www.rfc-editor.org\/info\/rfc2136  P. Vixie. 1997. Dynamic Updates in the Domain Name System (DNS UPDATE). RFC 2136. https:\/\/www.rfc-editor.org\/info\/rfc2136"},{"key":"e_1_3_2_1_56_1","unstructured":"Jianan Yao Runzhou Tao Ronghui Gu and Jason Nieh. 2022. {DuoAI}: Fast Automated Inference of Inductive Invariants for Verifying Distributed Protocols. In USENIX OSDI.  Jianan Yao Runzhou Tao Ronghui Gu and Jason Nieh. 2022. {DuoAI}: Fast Automated Inference of Inductive Invariants for Verifying Distributed Protocols. In USENIX OSDI."},{"key":"e_1_3_2_1_57_1","doi-asserted-by":"crossref","unstructured":"Arseniy Zaostrovnykh Solal Pirelli Luis Pedrosa Katerina Argyraki and George Candea. 2017. A formally verified NAT. In ACM SIGCOMM.  Arseniy Zaostrovnykh Solal Pirelli Luis Pedrosa Katerina Argyraki and George Candea. 2017. A formally verified NAT. In ACM SIGCOMM.","DOI":"10.1145\/3098822.3098833"},{"key":"e_1_3_2_1_58_1","doi-asserted-by":"crossref","unstructured":"Mo Zou Haoran Ding Dong Du Ming Fu Ronghui Gu and Haibo Chen. 2019. Using concurrent relational logic with helpers for verifying the AtomFS file system. In ACM SOSP.  Mo Zou Haoran Ding Dong Du Ming Fu Ronghui Gu and Haibo Chen. 2019. Using concurrent relational logic with helpers for verifying the AtomFS file system. In ACM SOSP.","DOI":"10.1145\/3341301.3359644"}],"event":{"name":"SOSP '23: 29th Symposium on Operating Systems Principles","location":"Koblenz Germany","acronym":"SOSP '23","sponsor":["SIGOPS ACM Special Interest Group on Operating Systems","USENIX"]},"container-title":["Proceedings of the 29th Symposium on Operating Systems Principles"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3600006.3613153","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:36:49Z","timestamp":1750178209000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3600006.3613153"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,10,23]]},"references-count":58,"alternative-id":["10.1145\/3600006.3613153","10.1145\/3600006"],"URL":"https:\/\/doi.org\/10.1145\/3600006.3613153","relation":{},"subject":[],"published":{"date-parts":[[2023,10,23]]},"assertion":[{"value":"2023-10-23","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}