{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,17]],"date-time":"2026-07-17T02:29:15Z","timestamp":1784255355894,"version":"3.55.0"},"reference-count":60,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2023,1,9]],"date-time":"2023-01-09T00:00:00Z","timestamp":1673222400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["101002277,789108"],"award-info":[{"award-number":["101002277,789108"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,1,9]]},"abstract":"<jats:p>Despite significant progress in the verification of hypervisors, operating systems, and compilers, and in verification tooling, there exists a wide gap between the approaches used in verification projects and conventional development of systems software. We see two main challenges in bringing these closer together: verification handling the complexity of code and semantics of conventional systems software, and verification usability.<\/jats:p>\n          <jats:p>We describe an experiment in verification tool design aimed at addressing some aspects of both: we design and implement CN, a separation-logic refinement type system for C systems software, aimed at predictable proof automation, based on a realistic semantics of ISO C. CN reduces refinement typing to decidable propositional logic reasoning, uses first-class resources to support pointer aliasing and pointer arithmetic, features resource inference for iterated separating conjunction, and uses a novel syntactic restriction of ghost variables in specifications to guarantee their successful inference. We implement CN and formalise key aspects of the type system, including a soundness proof of type checking. To demonstrate the usability of CN we use it to verify a substantial component of Google's pKVM hypervisor for Android.<\/jats:p>","DOI":"10.1145\/3571194","type":"journal-article","created":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T21:58:14Z","timestamp":1673474294000},"page":"1-32","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":21,"title":["CN: Verifying Systems C Code with Separation-Logic Refinement Types"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7369-183X","authenticated-orcid":false,"given":"Christopher","family":"Pulte","sequence":"first","affiliation":[{"name":"University of Cambridge, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7220-4991","authenticated-orcid":false,"given":"Dhruv C.","family":"Makwana","sequence":"additional","affiliation":[{"name":"University of Cambridge, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4891-0797","authenticated-orcid":false,"given":"Thomas","family":"Sewell","sequence":"additional","affiliation":[{"name":"University of Cambridge, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3723-636X","authenticated-orcid":false,"given":"Kayvan","family":"Memarian","sequence":"additional","affiliation":[{"name":"University of Cambridge, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9352-1013","authenticated-orcid":false,"given":"Peter","family":"Sewell","sequence":"additional","affiliation":[{"name":"University of Cambridge, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2838-5865","authenticated-orcid":false,"given":"Neel","family":"Krishnaswami","sequence":"additional","affiliation":[{"name":"University of Cambridge, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2023,1,11]]},"reference":[{"key":"e_1_2_1_1_1","first-page":"397","article-title":"L^ 3","volume":"77","author":"Ahmed Amal","year":"2007","unstructured":"Amal Ahmed , Matthew Fluet , and Greg Morrisett . 2007 . L^ 3 : A Linear Language with Locations. Fundam. Informaticae , 77 , 4 (2007), 397 \u2013 449 . Amal Ahmed, Matthew Fluet, and Greg Morrisett. 2007. L^ 3: A Linear Language with Locations. Fundam. Informaticae, 77, 4 (2007), 397\u2013449.","journal-title":"A Linear Language with Locations. Fundam. Informaticae"},{"key":"e_1_2_1_2_1","volume-title":"Foundational and Practical Aspects of Resource Analysis - Third International Workshop, FOPARA 2013","author":"Amadio Roberto M.","year":"2013","unstructured":"Roberto M. Amadio , Nicholas Ayache , Fran\u00e7ois Bobot , Jaap Boender , Brian Campbell , Ilias Garnier , Antoine Madet , James McKinna , Dominic P. Mulligan , Mauro Piccolo , Randy Pollack , Yann R\u00e9gis-Gianas , Claudio Sacerdoti Coen , Ian Stark , and Paolo Tranquilli . 2013 . Certified Complexity (CerCo) . In Foundational and Practical Aspects of Resource Analysis - Third International Workshop, FOPARA 2013 , Bertinoro, Italy , August 29-31, 2013, Revised Selected Papers. 1\u201318. https:\/\/doi.org\/10.1007\/978-3-319-12466-7_1 10.1007\/978-3-319-12466-7_1 10.1007\/978-3-319-12466-7_1 Roberto M. Amadio, Nicholas Ayache, Fran\u00e7ois Bobot, Jaap Boender, Brian Campbell, Ilias Garnier, Antoine Madet, James McKinna, Dominic P. Mulligan, Mauro Piccolo, Randy Pollack, Yann R\u00e9gis-Gianas, Claudio Sacerdoti Coen, Ian Stark, and Paolo Tranquilli. 2013. Certified Complexity (CerCo). In Foundational and Practical Aspects of Resource Analysis - Third International Workshop, FOPARA 2013, Bertinoro, Italy, August 29-31, 2013, Revised Selected Papers. 1\u201318. https:\/\/doi.org\/10.1007\/978-3-319-12466-7_1 10.1007\/978-3-319-12466-7_1"},{"key":"e_1_2_1_3_1","volume-title":"Android 13 Release Notes. https:\/\/source.android.com\/docs\/setup\/about\/android-13-release [Online","author":"Source Android Open","year":"2022","unstructured":"Android Open Source . 2022. Android 13 Release Notes. https:\/\/source.android.com\/docs\/setup\/about\/android-13-release [Online ; accessed 11- November - 2022 ] Android Open Source. 2022. Android 13 Release Notes. https:\/\/source.android.com\/docs\/setup\/about\/android-13-release [Online; accessed 11-November-2022]"},{"key":"#cr-split#-e_1_2_1_4_1.1","doi-asserted-by":"crossref","unstructured":"Andrew W. Appel Robert Dockins Aquinas Hobor Lennart Beringer Josiah Dodds Gordon Stewart Sandrine Blazy and Xavier Leroy. 2014. Program Logics for Certified Compilers. CUP. https:\/\/doi.org\/10.1017\/CBO9781107256552 10.1017\/CBO9781107256552 10.1017\/CBO9781107256552","DOI":"10.1017\/CBO9781107256552"},{"key":"#cr-split#-e_1_2_1_4_1.2","doi-asserted-by":"crossref","unstructured":"Andrew W. Appel Robert Dockins Aquinas Hobor Lennart Beringer Josiah Dodds Gordon Stewart Sandrine Blazy and Xavier Leroy. 2014. Program Logics for Certified Compilers. CUP. https:\/\/doi.org\/10.1017\/CBO9781107256552 10.1017\/CBO9781107256552","DOI":"10.1017\/CBO9781107256552"},{"key":"e_1_2_1_5_1","volume-title":"Summers","author":"Astrauskas Vytautas","year":"2022","unstructured":"Vytautas Astrauskas , Aurel B\u00edl\u00fd , Jon\u00e1s Fiala , Zachary Grannan , Christoph Matheja , Peter M\u00fcller , Federico Poli , and Alexander J . Summers . 2022 . The Prusti Project: Formal Verification for Rust. In NFM (Lecture Notes in Computer Science , Vol. 13260). Springer, 88\u2013 108 . Vytautas Astrauskas, Aurel B\u00edl\u00fd, Jon\u00e1s Fiala, Zachary Grannan, Christoph Matheja, Peter M\u00fcller, Federico Poli, and Alexander J. Summers. 2022. The Prusti Project: Formal Verification for Rust. In NFM (Lecture Notes in Computer Science, Vol. 13260). Springer, 88\u2013108."},{"key":"e_1_2_1_6_1","volume-title":"Robert DeLine, Bart Jacobs, and K. Rustan M. Leino.","author":"Barnett Michael","year":"2005","unstructured":"Michael Barnett , Bor-Yuh Evan Chang , Robert DeLine, Bart Jacobs, and K. Rustan M. Leino. 2005 . Boogie : A Modular Reusable Verifier for Object-Oriented Programs. In FMCO (Lecture Notes in Computer Science , Vol. 4111). Springer, 364\u2013 387 . Michael Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, and K. Rustan M. Leino. 2005. Boogie: A Modular Reusable Verifier for Object-Oriented Programs. In FMCO (Lecture Notes in Computer Science, Vol. 4111). Springer, 364\u2013387."},{"key":"e_1_2_1_7_1","doi-asserted-by":"crossref","first-page":"56","DOI":"10.1145\/3470569","article-title":"The dogged pursuit of bug-free C programs: the Frama-C software analysis platform","volume":"64","author":"Baudin Patrick","year":"2021","unstructured":"Patrick Baudin , Fran\u00e7ois Bobot , David B\u00fchler , Lo\u00efc Correnson , Florent Kirchner , Nikolai Kosmatov , Andr\u00e9 Maroneze , Valentin Perrelle , Virgile Prevosto , Julien Signoles , and Nicky Williams . 2021 . The dogged pursuit of bug-free C programs: the Frama-C software analysis platform . Commun. ACM , 64 , 8 (2021), 56 \u2013 68 . Patrick Baudin, Fran\u00e7ois Bobot, David B\u00fchler, Lo\u00efc Correnson, Florent Kirchner, Nikolai Kosmatov, Andr\u00e9 Maroneze, Valentin Perrelle, Virgile Prevosto, Julien Signoles, and Nicky Williams. 2021. The dogged pursuit of bug-free C programs: the Frama-C software analysis platform. Commun. ACM, 64, 8 (2021), 56\u201368.","journal-title":"Commun. ACM"},{"key":"e_1_2_1_8_1","volume-title":"European Conference on Networks and Communications, EuCNC 2016","author":"Baumann Christoph","year":"2016","unstructured":"Christoph Baumann , Mats N\u00e4slund , Christian Gehrmann , Oliver Schwarz , and Hans Thorsen . 2016 . A high assurance virtualization platform for ARMv8 . In European Conference on Networks and Communications, EuCNC 2016 , Athens, Greece , June 27-30, 2016. 210\u2013214. https:\/\/doi.org\/10.1109\/EuCNC.2016.7561034 10.1109\/EuCNC.2016.7561034 10.1109\/EuCNC.2016.7561034 Christoph Baumann, Mats N\u00e4slund, Christian Gehrmann, Oliver Schwarz, and Hans Thorsen. 2016. A high assurance virtualization platform for ARMv8. In European Conference on Networks and Communications, EuCNC 2016, Athens, Greece, June 27-30, 2016. 210\u2013214. https:\/\/doi.org\/10.1109\/EuCNC.2016.7561034 10.1109\/EuCNC.2016.7561034"},{"key":"e_1_2_1_9_1","volume-title":"O\u2019Hearn","author":"Berdine Josh","year":"2005","unstructured":"Josh Berdine , Cristiano Calcagno , and Peter W . O\u2019Hearn . 2005 . Smallfoot : Modular Automatic Assertion Checking with Separation Logic. In FMCO (Lecture Notes in Computer Science , Vol. 4111). Springer, 115\u2013 137 . Josh Berdine, Cristiano Calcagno, and Peter W. O\u2019Hearn. 2005. Smallfoot: Modular Automatic Assertion Checking with Separation Logic. In FMCO (Lecture Notes in Computer Science, Vol. 4111). Springer, 115\u2013137."},{"key":"e_1_2_1_10_1","volume-title":"7th International Conference, VMCAI 2006, Charleston, SC, USA, January 8-10, 2006, Proceedings, E. Allen Emerson and Kedar S. Namjoshi (Eds.) (Lecture Notes in Computer Science","volume":"442","author":"Bradley Aaron R.","unstructured":"Aaron R. Bradley , Zohar Manna , and Henny B. Sipma . 2006. What\u2019s Decidable About Arrays? In Verification, Model Checking, and Abstract Interpretation , 7th International Conference, VMCAI 2006, Charleston, SC, USA, January 8-10, 2006, Proceedings, E. Allen Emerson and Kedar S. Namjoshi (Eds.) (Lecture Notes in Computer Science , Vol. 3855). Springer, 427\u2013 442 . https:\/\/doi.org\/10.1007\/11609773_28 10.1007\/11609773_28 10.1007\/11609773_28 Aaron R. Bradley, Zohar Manna, and Henny B. Sipma. 2006. What\u2019s Decidable About Arrays? In Verification, Model Checking, and Abstract Interpretation, 7th International Conference, VMCAI 2006, Charleston, SC, USA, January 8-10, 2006, Proceedings, E. Allen Emerson and Kedar S. Namjoshi (Eds.) (Lecture Notes in Computer Science, Vol. 3855). Springer, 427\u2013442. https:\/\/doi.org\/10.1007\/11609773_28 10.1007\/11609773_28"},{"key":"e_1_2_1_11_1","doi-asserted-by":"crossref","unstructured":"James Brotherston Nikos Gorogiannis Max I. Kanovich and Reuben Rowe. 2016. Model checking for symbolic-heap separation logic with inductive predicates. In POPL. ACM 84\u201396. \t\t\t\t  James Brotherston Nikos Gorogiannis Max I. Kanovich and Reuben Rowe. 2016. Model checking for symbolic-heap separation logic with inductive predicates. In POPL. ACM 84\u201396.","DOI":"10.1145\/2914770.2837621"},{"key":"e_1_2_1_12_1","volume-title":"NASA Formal Methods (Lecture Notes in Computer Science","volume":"465","author":"Calcagno Cristiano","year":"2011","unstructured":"Cristiano Calcagno and Dino Distefano . 2011 . Infer: An Automatic Program Verifier for Memory Safety of C Programs . In NASA Formal Methods (Lecture Notes in Computer Science , Vol. 6617). Springer, 459\u2013 465 . Cristiano Calcagno and Dino Distefano. 2011. Infer: An Automatic Program Verifier for Memory Safety of C Programs. In NASA Formal Methods (Lecture Notes in Computer Science, Vol. 6617). Springer, 459\u2013465."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9457-5"},{"key":"e_1_2_1_14_1","volume-title":"FroCoS (Lecture Notes in Computer Science","volume":"320","author":"Cui Sa","year":"2005","unstructured":"Sa Cui , Kevin Donnelly , and Hongwei Xi . 2005 . ATS: A Language That Combines Programming with Theorem Proving . In FroCoS (Lecture Notes in Computer Science , Vol. 3717). Springer, 310\u2013 320 . Sa Cui, Kevin Donnelly, and Hongwei Xi. 2005. ATS: A Language That Combines Programming with Theorem Proving. In FroCoS (Lecture Notes in Computer Science, Vol. 3717). Springer, 310\u2013320."},{"key":"e_1_2_1_15_1","volume-title":"Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201908\/ETAPS\u201908)","author":"Moura Leonardo De","year":"2008","unstructured":"Leonardo De Moura and Nikolaj Bj\u00f8rner . 2008 . Z3: An Efficient SMT Solver . In Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201908\/ETAPS\u201908) . Springer-Verlag, Berlin, Heidelberg. 337\u2013340. isbn:3-540-78799-2, 978-3-540-78799-0 http:\/\/dl.acm.org\/citation.cfm?id=1792734.1792766 Leonardo De Moura and Nikolaj Bj\u00f8rner. 2008. Z3: An Efficient SMT Solver. In Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201908\/ETAPS\u201908). Springer-Verlag, Berlin, Heidelberg. 337\u2013340. isbn:3-540-78799-2, 978-3-540-78799-0 http:\/\/dl.acm.org\/citation.cfm?id=1792734.1792766"},{"key":"e_1_2_1_16_1","unstructured":"Will Deacon. 2020. Virtualisation for the Masses: Exposing KVM on Android. KVM Forum slides . https:\/\/mirrors.edge.kernel.org\/pub\/linux\/kernel\/people\/will\/slides\/kvmforum-2020-edited.pdf Accessed 2022-07-07 \t\t\t\t  Will Deacon. 2020. Virtualisation for the Masses: Exposing KVM on Android. KVM Forum slides . https:\/\/mirrors.edge.kernel.org\/pub\/linux\/kernel\/people\/will\/slides\/kvmforum-2020-edited.pdf Accessed 2022-07-07"},{"key":"e_1_2_1_17_1","unstructured":"Jake Edge. 2020. KVM for Android. Linux Weekly News . LWN article](https:\/\/lwn.net\/Articles\/836693\/ Accessed 2022-07-07 \t\t\t\t  Jake Edge. 2020. KVM for Android. Linux Weekly News . LWN article](https:\/\/lwn.net\/Articles\/836693\/ Accessed 2022-07-07"},{"key":"e_1_2_1_18_1","volume-title":"Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017","author":"Fox Anthony C. J.","year":"2017","unstructured":"Anthony C. J. Fox , Magnus O. Myreen , Yong Kiam Tan , and Ramana Kumar . 2017 . Verified compilation of CakeML to multiple machine-code targets . In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017 , Paris, France , January 16-17, 2017. 125\u2013137. https:\/\/doi.org\/10.1145\/3018610.3018621 10.1145\/3018610.3018621 10.1145\/3018610.3018621 Anthony C. J. Fox, Magnus O. Myreen, Yong Kiam Tan, and Ramana Kumar. 2017. Verified compilation of CakeML to multiple machine-code targets. In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017. 125\u2013137. https:\/\/doi.org\/10.1145\/3018610.3018621 10.1145\/3018610.3018621"},{"key":"e_1_2_1_19_1","volume-title":"Programming Languages and Systems - 28th European Symposium on Programming, ESOP","author":"Frumin Dan","year":"2019","unstructured":"Dan Frumin , L\u00e9on Gondelman , and Robbert Krebbers . 2019. Semi-automated Reasoning About Non-determinism in C Expressions . In Programming Languages and Systems - 28th European Symposium on Programming, ESOP 2019 , Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Lu\u00eds Caires (Ed.) (Lecture Notes in Computer Science , Vol. 11423). Springer, 60\u2013 87 . https:\/\/doi.org\/10.1007\/978-3-030-17184-1_3 10.1007\/978-3-030-17184-1_3 10.1007\/978-3-030-17184-1_3 Dan Frumin, L\u00e9on Gondelman, and Robbert Krebbers. 2019. Semi-automated Reasoning About Non-determinism in C Expressions. In Programming Languages and Systems - 28th European Symposium on Programming, ESOP 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Lu\u00eds Caires (Ed.) (Lecture Notes in Computer Science, Vol. 11423). Springer, 60\u201387. https:\/\/doi.org\/10.1007\/978-3-030-17184-1_3 10.1007\/978-3-030-17184-1_3"},{"key":"e_1_2_1_20_1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","article-title":"Linear Logic","volume":"50","author":"Girard Jean-Yves","year":"1987","unstructured":"Jean-Yves Girard . 1987 . Linear Logic . Theor. Comput. Sci. , 50 (1987), 1 \u2013 102 . Jean-Yves Girard. 1987. Linear Logic. Theor. Comput. Sci., 50 (1987), 1\u2013102.","journal-title":"Theor. Comput. Sci."},{"key":"e_1_2_1_21_1","volume-title":"CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In 12th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2016","author":"Gu Ronghui","year":"2016","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 12th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2016 , Savannah, GA, USA , November 2-4, 2016.. 653\u2013669. https:\/\/www.usenix.org\/conference\/osdi16\/technical-sessions\/presentation\/gu 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 12th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2016, Savannah, GA, USA, November 2-4, 2016.. 653\u2013669. https:\/\/www.usenix.org\/conference\/osdi16\/technical-sessions\/presentation\/gu"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-160558"},{"key":"e_1_2_1_23_1","volume-title":"11th USENIX Symposium on Operating Systems Design and Implementation, OSDI \u201914","author":"Hawblitzel Chris","year":"2014","unstructured":"Chris Hawblitzel , Jon Howell , Jacob R. Lorch , Arjun Narayan , Bryan Parno , Danfeng Zhang , and Brian Zill . 2014 . Ironclad Apps: End-to-End Security via Automated Full-System Verification . In 11th USENIX Symposium on Operating Systems Design and Implementation, OSDI \u201914 , Broomfield, CO, USA , October 6-8, 2014, Jason Flinn and Hank Levy (Eds.). USENIX Association, 165\u2013181. https:\/\/www.usenix.org\/conference\/osdi14\/technical-sessions\/presentation\/hawblitzel Chris Hawblitzel, Jon Howell, Jacob R. Lorch, Arjun Narayan, Bryan Parno, Danfeng Zhang, and Brian Zill. 2014. Ironclad Apps: End-to-End Security via Automated Full-System Verification. In 11th USENIX Symposium on Operating Systems Design and Implementation, OSDI \u201914, Broomfield, CO, USA, October 6-8, 2014, Jason Flinn and Hank Levy (Eds.). USENIX Association, 165\u2013181. https:\/\/www.usenix.org\/conference\/osdi14\/technical-sessions\/presentation\/hawblitzel"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3378426"},{"key":"e_1_2_1_25_1","volume-title":"Sound, Predictable, Fast Verifier for C and Java","author":"Jacobs Bart","year":"2039","unstructured":"Bart Jacobs , Jan Smans , Pieter Philippaerts , Fr\u00e9d\u00e9ric Vogels , Willem Penninckx , and Frank Piessens . 2011. VeriFast : A Powerful , Sound, Predictable, Fast Verifier for C and Java . In NASA Formal Methods, Mihaela Bobaru, Klaus Havelund, Gerard J. Holzmann, and Rajeev Joshi (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg . 41\u201355. isbn:978-3-642- 2039 8-5 Bart Jacobs, Jan Smans, Pieter Philippaerts, Fr\u00e9d\u00e9ric Vogels, Willem Penninckx, and Frank Piessens. 2011. VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java. In NASA Formal Methods, Mihaela Bobaru, Klaus Havelund, Gerard J. Holzmann, and Rajeev Joshi (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 41\u201355. isbn:978-3-642-20398-5"},{"key":"e_1_2_1_26_1","doi-asserted-by":"crossref","first-page":"e20","DOI":"10.1017\/S0956796818000151","article-title":"Iris from the ground up: A modular foundation for higher-order concurrent separation logic","volume":"28","author":"Jung Ralf","year":"2018","unstructured":"Ralf Jung , Robbert Krebbers , Jacques-Henri Jourdan , Ales Bizjak , Lars Birkedal , and Derek Dreyer . 2018 . Iris from the ground up: A modular foundation for higher-order concurrent separation logic . J. Funct. Program. , 28 (2018), e20 . Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ales Bizjak, Lars Birkedal, and Derek Dreyer. 2018. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. J. Funct. Program., 28 (2018), e20.","journal-title":"J. Funct. Program."},{"key":"e_1_2_1_27_1","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1145\/1743546.1743574","article-title":"seL4: formal verification of an operating-system kernel","volume":"53","author":"Klein Gerwin","year":"2010","unstructured":"Gerwin Klein , June Andronick , Kevin Elphinstone , Gernot Heiser , David Cock , Philip Derrin , Dhammika Elkaduwe , Kai Engelhardt , Rafal Kolanski , Michael Norrish , Thomas Sewell , Harvey Tuch , and Simon Winwood . 2010 . seL4: formal verification of an operating-system kernel . Commun. ACM , 53 , 6 (2010), 107 \u2013 115 . Gerwin Klein, June Andronick, Kevin Elphinstone, Gernot Heiser, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. 2010. seL4: formal verification of an operating-system kernel. Commun. ACM, 53, 6 (2010), 107\u2013115.","journal-title":"Commun. ACM"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2560537"},{"key":"e_1_2_1_29_1","volume-title":"The C Standard Formalized in Coq. Ph. D. Dissertation","author":"Krebbers Robbert","unstructured":"Robbert Krebbers . 2015. The C Standard Formalized in Coq. Ph. D. Dissertation . Radboud University Nijmegen . Robbert Krebbers. 2015. The C Standard Formalized in Coq. Ph. D. Dissertation. Radboud University Nijmegen."},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-016-9369-1"},{"key":"e_1_2_1_31_1","volume-title":"Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL \u201914)","author":"Kumar Ramana","year":"2014","unstructured":"Ramana Kumar , Magnus O. Myreen , Michael Norrish , and Scott Owens . 2014 . CakeML: A Verified Implementation of ML . In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL \u201914) . ACM, New York, NY, USA. 179\u2013191. isbn:978-1-4503-2544-8 https:\/\/doi.org\/10.1145\/2535838.2535841 10.1145\/2535838.2535841 10.1145\/2535838.2535841 Ramana Kumar, Magnus O. Myreen, Michael Norrish, and Scott Owens. 2014. CakeML: A Verified Implementation of ML. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL \u201914). ACM, New York, NY, USA. 179\u2013191. isbn:978-1-4503-2544-8 https:\/\/doi.org\/10.1145\/2535838.2535841 10.1145\/2535838.2535841"},{"key":"e_1_2_1_32_1","volume-title":"Verifying the Microsoft Hyper-V Hypervisor with VCC. In FM 2009: Formal Methods, Second World Congress, Eindhoven, The Netherlands, November 2-6, 2009. Proceedings. 806\u2013809","author":"Leinenbach Dirk","year":"2009","unstructured":"Dirk Leinenbach and Thomas Santen . 2009 . Verifying the Microsoft Hyper-V Hypervisor with VCC. In FM 2009: Formal Methods, Second World Congress, Eindhoven, The Netherlands, November 2-6, 2009. Proceedings. 806\u2013809 . https:\/\/doi.org\/10.1007\/978-3-642-05089-3_51 10.1007\/978-3-642-05089-3_51 10.1007\/978-3-642-05089-3_51 Dirk Leinenbach and Thomas Santen. 2009. Verifying the Microsoft Hyper-V Hypervisor with VCC. In FM 2009: Formal Methods, Second World Congress, Eindhoven, The Netherlands, November 2-6, 2009. Proceedings. 806\u2013809. https:\/\/doi.org\/10.1007\/978-3-642-05089-3_51 10.1007\/978-3-642-05089-3_51"},{"key":"e_1_2_1_33_1","volume-title":"RefinedC formalisation of the early allocator. https:\/\/gitlab.mpi-sws.org\/iris\/refinedc\/-\/tree\/master\/linux\/pkvm [Online","author":"Lepigre Rodolphe","year":"2022","unstructured":"Rodolphe Lepigre and Michael Sammler . 2022. RefinedC formalisation of the early allocator. https:\/\/gitlab.mpi-sws.org\/iris\/refinedc\/-\/tree\/master\/linux\/pkvm [Online ; accessed 24- October - 2022 ] Rodolphe Lepigre and Michael Sammler. 2022. RefinedC formalisation of the early allocator. https:\/\/gitlab.mpi-sws.org\/iris\/refinedc\/-\/tree\/master\/linux\/pkvm [Online; accessed 24-October-2022]"},{"key":"e_1_2_1_34_1","volume-title":"Proc. ACM Program. Lang., 6, POPL","author":"Lepigre Rodolphe","year":"2022","unstructured":"Rodolphe Lepigre , Michael Sammler , Kayvan Memarian , Robbert Krebbers , Derek Dreyer , and Peter Sewell . 2022 . VIP: verifying real-world C idioms with integer-pointer casts . Proc. ACM Program. Lang., 6, POPL (2022), 1\u201332. https:\/\/doi.org\/10.1145\/3498681 10.1145\/3498681 10.1145\/3498681 Rodolphe Lepigre, Michael Sammler, Kayvan Memarian, Robbert Krebbers, Derek Dreyer, and Peter Sewell. 2022. VIP: verifying real-world C idioms with integer-pointer casts. Proc. ACM Program. Lang., 6, POPL (2022), 1\u201332. https:\/\/doi.org\/10.1145\/3498681 10.1145\/3498681"},{"key":"e_1_2_1_35_1","doi-asserted-by":"crossref","unstructured":"Xavier Leroy. 2006. Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In POPL. ACM 42\u201354. \t\t\t\t  Xavier Leroy. 2006. Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In POPL. ACM 42\u201354.","DOI":"10.1145\/1111320.1111042"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9155-4"},{"key":"e_1_2_1_37_1","volume-title":"42nd IEEE Symposium on Security and Privacy, SP 2021","author":"Li Shih-Wei","year":"2021","unstructured":"Shih-Wei Li , Xupeng Li , Ronghui Gu , Jason Nieh , and John Zhuang Hui . 2021 . A Secure and Formally Verified Linux KVM Hypervisor . In 42nd IEEE Symposium on Security and Privacy, SP 2021 , San Francisco, CA, USA , 24-27 May 2021. IEEE, 1782\u20131799. https:\/\/doi.org\/10.1109\/SP40001.2021.00049 10.1109\/SP40001.2021.00049 10.1109\/SP40001.2021.00049 Shih-Wei Li, Xupeng Li, Ronghui Gu, Jason Nieh, and John Zhuang Hui. 2021. A Secure and Formally Verified Linux KVM Hypervisor. In 42nd IEEE Symposium on Security and Privacy, SP 2021, San Francisco, CA, USA, 24-27 May 2021. IEEE, 1782\u20131799. https:\/\/doi.org\/10.1109\/SP40001.2021.00049 10.1109\/SP40001.2021.00049"},{"key":"e_1_2_1_38_1","volume-title":"Sacha-\u00c9lie Ayoun, and Philippa Gardner.","author":"Maksimovic Petar","year":"2021","unstructured":"Petar Maksimovic , Jos\u00e9 Fragoso Santos , Sacha-\u00c9lie Ayoun, and Philippa Gardner. 2021 . Gillian : A Multi-Language Platform for Unified Symbolic Analysis. CoRR , abs\/2105.14769 (2021). Petar Maksimovic, Jos\u00e9 Fragoso Santos, Sacha-\u00c9lie Ayoun, and Philippa Gardner. 2021. Gillian: A Multi-Language Platform for Unified Symbolic Analysis. CoRR, abs\/2105.14769 (2021)."},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/MSEC.2022.3158196"},{"key":"e_1_2_1_40_1","volume-title":"Proceedings of the 2014 ACM SIGAda annual conference on High integrity language technology, HILT 2014","author":"Nicholas","year":"2014","unstructured":"Nicholas D. Matsakis and Felix S. Klock II. 2014. The Rust language . In Proceedings of the 2014 ACM SIGAda annual conference on High integrity language technology, HILT 2014 , Portland, Oregon, USA , October 18-21, 2014 , Michael Feldman and S. Tucker Taft (Eds.). ACM, 103\u2013104. https:\/\/doi.org\/10.1145\/2663171.2663188 10.1145\/2663171.2663188 10.1145\/2663171.2663188 Nicholas D. Matsakis and Felix S. Klock II. 2014. The Rust language. In Proceedings of the 2014 ACM SIGAda annual conference on High integrity language technology, HILT 2014, Portland, Oregon, USA, October 18-21, 2014, Michael Feldman and S. Tucker Taft (Eds.). ACM, 103\u2013104. https:\/\/doi.org\/10.1145\/2663171.2663188 10.1145\/2663171.2663188"},{"key":"e_1_2_1_41_1","volume-title":"Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015","author":"Melli\u00e8s Paul-Andr\u00e9","year":"2015","unstructured":"Paul-Andr\u00e9 Melli\u00e8s and Noam Zeilberger . 2015 . Functors are Type Refinement Systems . In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015 , Mumbai, India , January 15-17, 2015, Sriram K. Rajamani and David Walker (Eds.). ACM, 3\u201316. https:\/\/doi.org\/10.1145\/2676726.2676970 10.1145\/2676726.2676970 10.1145\/2676726.2676970 Paul-Andr\u00e9 Melli\u00e8s and Noam Zeilberger. 2015. Functors are Type Refinement Systems. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015, Sriram K. Rajamani and David Walker (Eds.). ACM, 3\u201316. https:\/\/doi.org\/10.1145\/2676726.2676970 10.1145\/2676726.2676970"},{"key":"e_1_2_1_42_1","volume-title":"Proceedings of the 46th ACM SIGPLAN Symposium on Principles of Programming Languages. https:\/\/doi.org\/10.1145\/3290380 Proc. ACM Program. Lang. 3, POPL, Article 67","author":"Memarian Kayvan","year":"2019","unstructured":"Kayvan Memarian , Victor B. F. Gomes , Brooks Davis , Stephen Kell , Alexander Richardson , Robert N. M. Watson , and Peter Sewell . 2019 . Exploring C Semantics and Pointer Provenance . In Proceedings of the 46th ACM SIGPLAN Symposium on Principles of Programming Languages. https:\/\/doi.org\/10.1145\/3290380 Proc. ACM Program. Lang. 3, POPL, Article 67 . Also available as ISO\/IEC JTC1\/SC22\/WG14 N2311 10.1145\/3290380 10.1145\/3290380 Kayvan Memarian, Victor B. F. Gomes, Brooks Davis, Stephen Kell, Alexander Richardson, Robert N. M. Watson, and Peter Sewell. 2019. Exploring C Semantics and Pointer Provenance. In Proceedings of the 46th ACM SIGPLAN Symposium on Principles of Programming Languages. https:\/\/doi.org\/10.1145\/3290380 Proc. ACM Program. Lang. 3, POPL, Article 67. Also available as ISO\/IEC JTC1\/SC22\/WG14 N2311 10.1145\/3290380"},{"key":"e_1_2_1_43_1","volume-title":"Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016","author":"Memarian Kayvan","year":"2016","unstructured":"Kayvan Memarian , Justus Matthiesen , James Lingard , Kyndylan Nienhuis , David Chisnall , Robert N. M. Watson , and Peter Sewell . 2016 . Into the depths of C: elaborating the de facto standards . In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016 , Santa Barbara, CA, USA , June 13-17, 2016, Chandra Krintz and Emery D. Berger (Eds.). ACM, 1\u201315. https:\/\/doi.org\/10.1145\/2908080.2908081 10.1145\/2908080.2908081 10.1145\/2908080.2908081 Kayvan Memarian, Justus Matthiesen, James Lingard, Kyndylan Nienhuis, David Chisnall, Robert N. M. Watson, and Peter Sewell. 2016. Into the depths of C: elaborating the de facto standards. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, Santa Barbara, CA, USA, June 13-17, 2016, Chandra Krintz and Emery D. Berger (Eds.). ACM, 1\u201315. https:\/\/doi.org\/10.1145\/2908080.2908081 10.1145\/2908080.2908081"},{"key":"e_1_2_1_44_1","volume-title":"CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I, Swarat Chaudhuri and Azadeh Farzan (Eds.) (Lecture Notes in Computer Science","volume":"425","author":"M\u00fcller Peter","unstructured":"Peter M\u00fcller , Malte Schwerhoff , and Alexander J. Summers . 2016. Automatic Verification of Iterated Separating Conjunctions Using Symbolic Execution. In Computer Aided Verification - 28th International Conference , CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I, Swarat Chaudhuri and Azadeh Farzan (Eds.) (Lecture Notes in Computer Science , Vol. 9779). Springer, 405\u2013 425 . https:\/\/doi.org\/10.1007\/978-3-319-41528-4_22 10.1007\/978-3-319-41528-4_22 10.1007\/978-3-319-41528-4_22 Peter M\u00fcller, Malte Schwerhoff, and Alexander J. Summers. 2016. Automatic Verification of Iterated Separating Conjunctions Using Symbolic Execution. In Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I, Swarat Chaudhuri and Azadeh Farzan (Eds.) (Lecture Notes in Computer Science, Vol. 9779). Springer, 405\u2013425. https:\/\/doi.org\/10.1007\/978-3-319-41528-4_22 10.1007\/978-3-319-41528-4_22"},{"key":"e_1_2_1_45_1","volume-title":"Summers","author":"M\u00fcller Peter","year":"2017","unstructured":"Peter M\u00fcller , Malte Schwerhoff , and Alexander J . Summers . 2017 . Viper : A Verification Infrastructure for Permission-Based Reasoning. In Dependable Software Systems Engineering (NATO Science for Peace and Security Series - D: Information and Communication Security , Vol. 50). IOS Press, 104\u2013 125 . Peter M\u00fcller, Malte Schwerhoff, and Alexander J. Summers. 2017. Viper: A Verification Infrastructure for Permission-Based Reasoning. In Dependable Software Systems Engineering (NATO Science for Peace and Security Series - D: Information and Communication Security, Vol. 50). IOS Press, 104\u2013125."},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45937-5_16"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679682100023X"},{"key":"#cr-split#-e_1_2_1_48_1.1","unstructured":"Christopher Pulte Dhruv C. Makwana Thomas Sewell Kayvan Memarian Peter Sewell and Neel Krishnaswami. 2022. Data for \"CN: Verifying Systems C Code with Separation-Logic Refinement Types\". https:\/\/doi.org\/10.5281\/zenodo.7320414 10.5281\/zenodo.7320414 10.5281\/zenodo.7320414"},{"key":"#cr-split#-e_1_2_1_48_1.2","unstructured":"Christopher Pulte Dhruv C. Makwana Thomas Sewell Kayvan Memarian Peter Sewell and Neel Krishnaswami. 2022. Data for \"CN: Verifying Systems C Code with Separation-Logic Refinement Types\". https:\/\/doi.org\/10.5281\/zenodo.7320414 10.5281\/zenodo.7320414"},{"key":"e_1_2_1_49_1","volume-title":"Syntactic Control of Interference","author":"Reynolds John C.","unstructured":"John C. Reynolds . 1978. Syntactic Control of Interference . In POPL. ACM Press , 39\u201346. John C. Reynolds. 1978. Syntactic Control of Interference. In POPL. ACM Press, 39\u201346."},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_2_1_51_1","volume-title":"An Introduction to Separation Logic (Preliminary Draft). \". https:\/\/www.cs.cmu.edu\/ jcr\/copenhagen08.pdf \"[Online","author":"Reynolds John C.","year":"2022","unstructured":"John C. Reynolds . 2008. An Introduction to Separation Logic (Preliminary Draft). \". https:\/\/www.cs.cmu.edu\/ jcr\/copenhagen08.pdf \"[Online ; accessed 4- July - 2022 ]\" John C. Reynolds. 2008. An Introduction to Separation Logic (Preliminary Draft). \". https:\/\/www.cs.cmu.edu\/ jcr\/copenhagen08.pdf \"[Online; accessed 4-July-2022]\""},{"key":"e_1_2_1_52_1","doi-asserted-by":"crossref","unstructured":"Patrick Maxim Rondon Ming Kawaguchi and Ranjit Jhala. 2008. Liquid types. In PLDI. ACM 159\u2013169. \t\t\t\t  Patrick Maxim Rondon Ming Kawaguchi and Ranjit Jhala. 2008. Liquid types. In PLDI. ACM 159\u2013169.","DOI":"10.1145\/1379022.1375602"},{"key":"e_1_2_1_53_1","volume-title":"43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation","author":"Sammler Michael","year":"2022","unstructured":"Michael Sammler , Angus Hammond , Rodolphe Lepigre , Brian Campbell , Jean Pichon-Pharabod , Derek Dreyer , Deepak Garg , and Peter Sewell . 2022 . Islaris: verification of machine code against authoritative ISA semantics. In PLDI \u201922 : 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation , San Diego, CA, USA, June 13 - 17 , 2022, Ranjit Jhala and Isil Dillig (Eds.). ACM, 825\u2013840. https:\/\/doi.org\/10.1145\/3519939.3523434 10.1145\/3519939.3523434 10.1145\/3519939.3523434 Michael Sammler, Angus Hammond, Rodolphe Lepigre, Brian Campbell, Jean Pichon-Pharabod, Derek Dreyer, Deepak Garg, and Peter Sewell. 2022. Islaris: verification of machine code against authoritative ISA semantics. In PLDI \u201922: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, San Diego, CA, USA, June 13 - 17, 2022, Ranjit Jhala and Isil Dillig (Eds.). ACM, 825\u2013840. https:\/\/doi.org\/10.1145\/3519939.3523434 10.1145\/3519939.3523434"},{"key":"e_1_2_1_54_1","volume-title":"42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation","author":"Sammler Michael","year":"2021","unstructured":"Michael Sammler , Rodolphe Lepigre , Robbert Krebbers , Kayvan Memarian , Derek Dreyer , and Deepak Garg . 2021 . RefinedC: automating the foundational verification of C code with refined ownership types. In PLDI \u201921 : 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation , Virtual Event, Canada , June 20-25, 2021, Stephen N. Freund and Eran Yahav (Eds.). ACM, 158\u2013174. https:\/\/doi.org\/10.1145\/3453483.3454036 10.1145\/3453483.3454036 10.1145\/3453483.3454036 Michael Sammler, Rodolphe Lepigre, Robbert Krebbers, Kayvan Memarian, Derek Dreyer, and Deepak Garg. 2021. RefinedC: automating the foundational verification of C code with refined ownership types. In PLDI \u201921: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Virtual Event, Canada, June 20-25, 2021, Stephen N. Freund and Eran Yahav (Eds.). ACM, 158\u2013174. https:\/\/doi.org\/10.1145\/3453483.3454036 10.1145\/3453483.3454036"},{"key":"e_1_2_1_55_1","volume-title":"43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). ACM, 256\u2013270","author":"Swamy Nikhil","year":"2016","unstructured":"Nikhil Swamy , Catalin Hritcu , Chantal Keller , Aseem Rastogi , Antoine Delignat-Lavaud , Simon Forest , Karthikeyan Bhargavan , C\u00e9dric Fournet , Pierre-Yves Strub , Markulf Kohlweiss , Jean-Karim Zinzindohou\u00e9 , and Santiago Zanella-B\u00e9guelin . 2016 . Dependent Types and Multi-Monadic Effects in F* . In 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). ACM, 256\u2013270 . isbn:978-1-4503-3549-2 https:\/\/www.fstar-lang.org\/papers\/mumon\/ Nikhil Swamy, Catalin Hritcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, C\u00e9dric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean-Karim Zinzindohou\u00e9, and Santiago Zanella-B\u00e9guelin. 2016. Dependent Types and Multi-Monadic Effects in F*. In 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). ACM, 256\u2013270. isbn:978-1-4503-3549-2 https:\/\/www.fstar-lang.org\/papers\/mumon\/"},{"key":"e_1_2_1_56_1","volume-title":"Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016","author":"Tan Yong Kiam","year":"2016","unstructured":"Yong Kiam Tan , Magnus O. Myreen , Ramana Kumar , Anthony C. J. Fox , Scott Owens , and Michael Norrish . 2016 . A new verified compiler backend for CakeML . In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016 , Nara, Japan , September 18-22, 2016. 60\u201373. https:\/\/doi.org\/10.1145\/2951913.2951924 10.1145\/2951913.2951924 10.1145\/2951913.2951924 Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, Anthony C. J. Fox, Scott Owens, and Michael Norrish. 2016. A new verified compiler backend for CakeML. In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18-22, 2016. 60\u201373. https:\/\/doi.org\/10.1145\/2951913.2951924 10.1145\/2951913.2951924"},{"key":"e_1_2_1_57_1","volume-title":"ACM SIGOPS 28th Symposium on Operating Systems Principles, Virtual Event \/ Koblenz","author":"Tao Runzhou","year":"2021","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 SOSP \u201921 : ACM SIGOPS 28th Symposium on Operating Systems Principles, Virtual Event \/ Koblenz , Germany, October 26-29, 2021, Robbert van Renesse and Nickolai Zeldovich (Eds.). ACM, 866\u2013881. https:\/\/doi.org\/10.1145\/3477132.3483560 10.1145\/3477132.3483560 10.1145\/3477132.3483560 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 SOSP \u201921: ACM SIGOPS 28th Symposium on Operating Systems Principles, Virtual Event \/ Koblenz, Germany, October 26-29, 2021, Robbert van Renesse and Nickolai Zeldovich (Eds.). ACM, 866\u2013881. https:\/\/doi.org\/10.1145\/3477132.3483560 10.1145\/3477132.3483560"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796806006216"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3571194","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3571194","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T18:08:21Z","timestamp":1750183701000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3571194"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,9]]},"references-count":60,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2023,1,9]]}},"alternative-id":["10.1145\/3571194"],"URL":"https:\/\/doi.org\/10.1145\/3571194","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,1,9]]},"assertion":[{"value":"2023-01-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}