{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,6]],"date-time":"2026-05-06T23:05:36Z","timestamp":1778108736363,"version":"3.51.4"},"publisher-location":"New York, NY, USA","reference-count":86,"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\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-1836724, CCF-1651225, CNS-1844807"],"award-info":[{"award-number":["CCF-1836724, CCF-1651225, CNS-1844807"]}],"id":[{"id":"10.13039\/100000001","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\/3341301.3359641","type":"proceedings-article","created":{"date-parts":[[2019,10,21]],"date-time":"2019-10-21T13:34:22Z","timestamp":1571664862000},"page":"225-242","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":67,"title":["Scaling symbolic evaluation for automated verification of systems code with Serval"],"prefix":"10.1145","author":[{"given":"Luke","family":"Nelson","sequence":"first","affiliation":[{"name":"University of Washington"}]},{"given":"James","family":"Bornholt","sequence":"additional","affiliation":[{"name":"University of Washington"}]},{"given":"Ronghui","family":"Gu","sequence":"additional","affiliation":[{"name":"Columbia University"}]},{"given":"Andrew","family":"Baumann","sequence":"additional","affiliation":[{"name":"Microsoft Research"}]},{"given":"Emina","family":"Torlak","sequence":"additional","affiliation":[{"name":"University of Washington"}]},{"given":"Xi","family":"Wang","sequence":"additional","affiliation":[{"name":"University of Washington"}]}],"member":"320","published-online":{"date-parts":[[2019,10,27]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15057-9_5"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2872362.2872404"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815420"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290384"},{"key":"e_1_3_2_1_5_1","volume-title":"Camil Demetrescu, and Irene Finocchi.","author":"Baldoni Roberto","year":"2018","unstructured":"Roberto Baldoni , Emilio Coppa , Daniele Cono D'elia , Camil Demetrescu, and Irene Finocchi. 2018 . A Survey of Symbolic Execution Techniques. ACM Computing Survey 51, 3, Article 50 (July 2018), 39 pages. Roberto Baldoni, Emilio Coppa, Daniele Cono D'elia, Camil Demetrescu, and Irene Finocchi. 2018. A Survey of Symbolic Execution Techniques. ACM Computing Survey 51, 3, Article 50 (July 2018), 39 pages."},{"key":"e_1_3_2_1_6_1","volume-title":"Proceedings of the 4th International Symposium on Formal Methods for Components and Objects","author":"Barnett Mike","year":"2005","unstructured":"Mike 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 Proceedings of the 4th International Symposium on Formal Methods for Components and Objects . Amsterdam, The Netherlands, 364--387. Mike 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 Proceedings of the 4th International Symposium on Formal Methods for Components and Objects. Amsterdam, The Netherlands, 364--387."},{"key":"e_1_3_2_1_7_1","volume-title":"Proceedings of the 10th USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Belay Adam","year":"2012","unstructured":"Adam Belay , Andrea Bittau , Ali Mashtizadeh , David Terei , David Mazi\u00e8res , and Christos Kozyrakis . 2012 . Dune: Safe User-level Access to Privileged CPU Features . In Proceedings of the 10th USENIX Symposium on Operating Systems Design and Implementation (OSDI) . Hollywood, CA, 335--348. Adam Belay, Andrea Bittau, Ali Mashtizadeh, David Terei, David Mazi\u00e8res, and Christos Kozyrakis. 2012. Dune: Safe User-level Access to Privileged CPU Features. In Proceedings of the 10th USENIX Symposium on Operating Systems Design and Implementation (OSDI). Hollywood, CA, 335--348."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.41331"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-006-0204-6"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/646483.691738"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9148-3"},{"key":"e_1_3_2_1_12_1","volume-title":"Proceedings of the 26th USENIX Security Symposium","author":"Bond Barry","year":"2017","unstructured":"Barry Bond , Chris Hawblitzel , Manos Kapritsos , K. Rustan M. Leino , Jacob R. Lorch , Bryan Parno , Ashay Rane , Srinath Setty , and Laure Thompson . 2017 . Vale: Verifying High-Performance Cryptographic Assembly Code . In Proceedings of the 26th USENIX Security Symposium . Vancouver, Canada, 917--934. Barry Bond, Chris Hawblitzel, Manos Kapritsos, K. Rustan M. Leino, Jacob R. Lorch, Bryan Parno, Ashay Rane, Srinath Setty, and Laure Thompson. 2017. Vale: Verifying High-Performance Cryptographic Assembly Code. In Proceedings of the 26th USENIX Security Symposium. Vancouver, Canada, 917--934."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276519"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/0898-1221(94)00215-7"},{"key":"e_1_3_2_1_15_1","volume-title":"Proceedings of the 27th USENIX Security Symposium","author":"Bulck Jo Van","year":"2018","unstructured":"Jo Van Bulck , Marina Minkin , Ofir Weisse , Daniel Genkin , Baris Kasikci , Frank Piessens , Mark Silberstein , Thomas F. Wenisch , Yuval Yarom , and Raoul Strackx . 2018 . Foreshadow: Extracting the Keys to the Intel SGX Kingdom with Transient Out-of-Order Execution . In Proceedings of the 27th USENIX Security Symposium . Baltimore, MD, 991--1008. Jo Van Bulck, Marina Minkin, Ofir Weisse, Daniel Genkin, Baris Kasikci, Frank Piessens, Mark Silberstein, Thomas F. Wenisch, Yuval Yarom, and Raoul Strackx. 2018. Foreshadow: Extracting the Keys to the Intel SGX Kingdom with Transient Out-of-Order Execution. In Proceedings of the 27th USENIX Security Symposium. Baltimore, MD, 991--1008."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2786805.2803205"},{"key":"e_1_3_2_1_17_1","volume-title":"Proceedings of the 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Cadar Cristian","year":"2008","unstructured":"Cristian Cadar , Daniel Dunbar , and Dawson Engler . 2008 . KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs . In Proceedings of the 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI) . San Diego, CA, 209--224. Cristian Cadar, Daniel Dunbar, and Dawson Engler. 2008. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In Proceedings of the 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI). San Diego, CA, 209--224."},{"key":"e_1_3_2_1_18_1","volume-title":"Proceedings of the 13th ACM Conference on Computer and Communications Security (CCS)","author":"Cadar Cristian","unstructured":"Cristian Cadar , Vijay Ganesh , Peter M. Pawlowski , David L. Dill , and Dawson R. Engler . 2006. EXE: Automatically Generating Inputs of Death . In Proceedings of the 13th ACM Conference on Computer and Communications Security (CCS) . Alexandria, VA, 322--335. Cristian Cadar, Vijay Ganesh, Peter M. Pawlowski, David L. Dill, and Dawson R. Engler. 2006. EXE: Automatically Generating Inputs of Death. In Proceedings of the 13th ACM Conference on Computer and Communications Security (CCS). Alexandria, VA, 322--335."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2408776.2408795"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594301"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132776"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815402"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1950365.1950396"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677003"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46081-8_21"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96142-2_26"},{"key":"e_1_3_2_1_27_1","volume-title":"A System to Generate Test Data and Symbolically Execute Programs. TSE 2, 3 (5","author":"Clarke Lori A.","year":"1976","unstructured":"Lori A. Clarke . 1976. A System to Generate Test Data and Symbolically Execute Programs. TSE 2, 3 (5 1976 ), 215--222. Lori A. Clarke. 1976. A System to Generate Test Data and Symbolically Execute Programs. TSE 2, 3 (5 1976), 215--222."},{"key":"e_1_3_2_1_28_1","unstructured":"Jonathan Corbet. 2015. Post-init read-only memory. https:\/\/lwn.net\/Articles\/666550\/.  Jonathan Corbet. 2015. Post-init read-only memory. https:\/\/lwn.net\/Articles\/666550\/."},{"key":"e_1_3_2_1_29_1","volume-title":"Proceedings of the 25th USENIX Security Symposium","author":"Costan Victor","year":"2016","unstructured":"Victor Costan , IliaLebedev, and Srinivas Devadas . 2016 . Sanctum: Minimal Hardware Extensions for Strong Software Isolation . In Proceedings of the 25th USENIX Security Symposium . Austin, TX, 857--874. Victor Costan, IliaLebedev, and Srinivas Devadas. 2016. Sanctum: Minimal Hardware Extensions for Strong Software Isolation. In Proceedings of the 25th USENIX Security Symposium. Austin, TX, 857--874."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908100"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14203-1_34"},{"key":"e_1_3_2_1_34_1","volume-title":"Proceedings of the 11th USENIX Symposium on Networked Systems Design and Implementation (NSDI)","author":"Dobrescu Mihai","year":"2014","unstructured":"Mihai Dobrescu and Katerina Argyraki . 2014 . Software Dataplane Verification . In Proceedings of the 11th USENIX Symposium on Networked Systems Design and Implementation (NSDI) . Seattle, WA, 101--114. Mihai Dobrescu and Katerina Argyraki. 2014. Software Dataplane Verification. In Proceedings of the 11th USENIX Symposium on Networked Systems Design and Implementation (NSDI). Seattle, WA, 101--114."},{"key":"e_1_3_2_1_35_1","first-page":"3","article-title":"A Programmable Programming","volume":"61","author":"Felleisen Matthias","year":"2018","unstructured":"Matthias Felleisen , Robert Bruce Findler , Matthew Flatt , Shriram Krishnamurthi , Eli Barzilay , Jay McCarthy , and Sam Tobin-Hochstadt . 2018 . A Programmable Programming Language. Commun. ACM 61 , 3 (March 2018), 62--71. Matthias Felleisen, Robert Bruce Findler, Matthew Flatt, Shriram Krishnamurthi, Eli Barzilay, Jay McCarthy, and Sam Tobin-Hochstadt. 2018. A Programmable Programming Language. Commun. ACM 61, 3 (March 2018), 62--71.","journal-title":"Language. Commun. ACM"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132782"},{"key":"e_1_3_2_1_37_1","unstructured":"Matt Fleming. 2017. A thorough introduction to eBPF. https:\/\/lwn.net\/Articles\/740157\/.  Matt Fleming. 2017. A thorough introduction to eBPF. https:\/\/lwn.net\/Articles\/740157\/."},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2093548.2093564"},{"key":"e_1_3_2_1_39_1","volume-title":"Proceedings of the 3rd IEEE Symposium on Security and Privacy","author":"Goguen J. A.","unstructured":"J. A. Goguen and J. Meseguer . 1982. Security Policies and Security Models . In Proceedings of the 3rd IEEE Symposium on Security and Privacy . Oakland, CA, 11--20. J. A. Goguen and J. Meseguer. 1982. Security Policies and Security Models. In Proceedings of the 3rd IEEE Symposium on Security and Privacy. Oakland, CA, 11--20."},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676975"},{"key":"e_1_3_2_1_41_1","volume-title":"Proceedings of the 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI)","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 Proceedings of the 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI) . Savannah, GA, 653--669. 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 Proceedings of the 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI). Savannah, GA, 653--669."},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815428"},{"key":"e_1_3_2_1_43_1","volume-title":"Proceedings of the 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI)","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 Proceedings of the 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI) . Broomfield, CO, 165--181. 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 Proceedings of the 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI). Broomfield, CO, 165--181."},{"key":"e_1_3_2_1_44_1","first-page":"4","article-title":"Lightweight Formal Methods","volume":"29","author":"Jackson Daniel","year":"1996","unstructured":"Daniel Jackson and Jeannette Wing . 1996 . Lightweight Formal Methods . IEEE Computer 29 , 4 (April 1996), 20--22. Daniel Jackson and Jeannette Wing. 1996. Lightweight Formal Methods. IEEE Computer 29, 4 (April 1996), 20--22.","journal-title":"IEEE Computer"},{"key":"e_1_3_2_1_45_1","volume-title":"Partial Evaluation and Automatic Program Generation","author":"Jones Neil D.","unstructured":"Neil D. Jones , Carsten K. Gomard , and Peter Sestoft . 1993. Partial Evaluation and Automatic Program Generation . Prentice Hall International . Neil D. Jones, Carsten K. Gomard, and Peter Sestoft. 1993. Partial Evaluation and Automatic Program Generation. Prentice Hall International."},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31365-3_27"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/s12046-009-0002-4"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2560537"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2019.00002"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254088"},{"key":"e_1_3_2_1_53_1","unstructured":"Leslie Lamport. 2008. Computation and State Machines.  Leslie Lamport. 2008. Computation and State Machines."},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.5555\/977395.977673"},{"key":"e_1_3_2_1_55_1","volume-title":"Keystone: A Framework for Architecting TEEs. https:\/\/arxiv.org\/abs\/1907.10119.","author":"Lee Dayeol","year":"2019","unstructured":"Dayeol Lee , David Kohlbrenner , Shweta Shinde , Dawn Song , and Krste Asanovi\u0107 . 2019 . Keystone: A Framework for Architecting TEEs. https:\/\/arxiv.org\/abs\/1907.10119. Dayeol Lee, David Kohlbrenner, Shweta Shinde, Dawn Song, and Krste Asanovi\u0107. 2019. Keystone: A Framework for Architecting TEEs. https:\/\/arxiv.org\/abs\/1907.10119."},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.5555\/1939141.1939161"},{"key":"e_1_3_2_1_57_1","volume-title":"Usable Auto-Active Verification. In Workshop on Usable Verification","author":"K. Rustan","unstructured":"K. Rustan M. Leino and Micha\u0142 Moskal. 2010 . Usable Auto-Active Verification. In Workshop on Usable Verification . Redmond, WA, 4. K. Rustan M. Leino and Micha\u0142 Moskal. 2010. Usable Auto-Active Verification. In Workshop on Usable Verification. Redmond, WA, 4."},{"key":"e_1_3_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040319"},{"key":"e_1_3_2_1_61_1","volume-title":"Proceedings of the 27th USENIX Security Symposium","author":"Lipp Moritz","year":"2018","unstructured":"Moritz Lipp , Michael Schwarz , Daniel Gruss , Thomas Prescher , Werner Haas , Anders Fogh , Jann Horn , Stefan Mangard , Paul Kocher , Daniel Genkin , Yuval Yarom , and Mike Hamburg . 2018 . Meltdown: Reading Kernel Memory from User Space . In Proceedings of the 27th USENIX Security Symposium . Baltimore, MD, 973--990. Moritz Lipp, Michael Schwarz, Daniel Gruss, Thomas Prescher, Werner Haas, Anders Fogh, Jann Horn, Stefan Mangard, Paul Kocher, Daniel Genkin, Yuval Yarom, and Mike Hamburg. 2018. Meltdown: Reading Kernel Memory from User Space. In Proceedings of the 27th USENIX Security Symposium. Baltimore, MD, 973--990."},{"key":"e_1_3_2_1_62_1","volume-title":"Proceedings of the 18th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS)","author":"Mai Haohui","unstructured":"Haohui Mai , Edgar Pek , Hui Xue , Samuel T. King , and P. Madhusudan . 2013. Verifying Security Invariants in ExpressOS . In Proceedings of the 18th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS) . Houston, TX, 293--304. Haohui Mai, Edgar Pek, Hui Xue, Samuel T. King, and P. Madhusudan. 2013. Verifying Security Invariants in ExpressOS. In Proceedings of the 18th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS). Houston, TX, 293--304."},{"key":"e_1_3_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/2948618.2954331"},{"key":"e_1_3_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2013.35"},{"key":"e_1_3_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132748"},{"key":"e_1_3_2_1_66_1","volume-title":"A Proof Assistant for Higher-Order Logic","author":"Nipkow Tobias","unstructured":"Tobias Nipkow , Lawrence C. Paulson , and Markus Wenzel . 2016. Isabelle\/HOL : A Proof Assistant for Higher-Order Logic . Springer-Verlag . Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. 2016. Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. Springer-Verlag."},{"key":"e_1_3_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951940"},{"key":"e_1_3_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41540-6_2"},{"key":"e_1_3_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133912"},{"key":"e_1_3_2_1_70_1","unstructured":"John Rushby. 1992. Noninterference Transitivity and Channel-Control Security Policies. Technical Report CSL-92-02. SRI International.  John Rushby. 1992. Noninterference Transitivity and Channel-Control Security Policies. Technical Report CSL-92-02. SRI International."},{"key":"e_1_3_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/1294261.1294294"},{"key":"e_1_3_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462183"},{"key":"e_1_3_2_1_73_1","volume-title":"SiFive U54 Core Complex Manual, v19.05. SiFive","unstructured":"SiFive. 2019. SiFive U54 Core Complex Manual, v19.05. SiFive , Inc . https:\/\/www.sifive.com\/cores\/u54 SiFive. 2019. SiFive U54 Core Complex Manual, v19.05. SiFive, Inc. https:\/\/www.sifive.com\/cores\/u54"},{"key":"e_1_3_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.5555\/3026877.3026879"},{"key":"e_1_3_2_1_75_1","volume-title":"Proceedings of the 13th USENIX Symposium on Operating Systems Design and Implementation (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 Proceedings of the 13th USENIX Symposium on Operating Systems Design and Implementation (OSDI) . Carlsbad, CA, 287--306. 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 Proceedings of the 13th USENIX Symposium on Operating Systems Design and Implementation (OSDI). Carlsbad, CA, 287--306."},{"key":"e_1_3_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.1145\/2814270.2814321"},{"key":"e_1_3_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.1007\/11547662_24"},{"key":"e_1_3_2_1_78_1","unstructured":"The Clang Team. 2019. UndefinedBehaviorSanitizer. https:\/\/clang.llvm.org\/docs\/UndefinedBehaviorSanitizer.html  The Clang Team. 2019. UndefinedBehaviorSanitizer. https:\/\/clang.llvm.org\/docs\/UndefinedBehaviorSanitizer.html"},{"key":"e_1_3_2_1_79_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.2554024"},{"key":"e_1_3_2_1_80_1","doi-asserted-by":"crossref","unstructured":"Emina Torlak and Rastislav Bodik. 2013. Growing Solver-Aided Languages with Rosette. In Onward! Boston MA 135--152.  Emina Torlak and Rastislav Bodik. 2013. Growing Solver-Aided Languages with Rosette. In Onward! Boston MA 135--152.","DOI":"10.1145\/2509578.2509586"},{"key":"e_1_3_2_1_81_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594340"},{"key":"e_1_3_2_1_82_1","volume-title":"Proceedings of the 14th Workshop on Hot Topics in Operating Systems (HotOS). Santa Ana Pueblo, NM, 6.","author":"Wagner Jonas","year":"2013","unstructured":"Jonas Wagner , Volodymyr Kuznetsov , and George Candea . 2013 . -Overify: Optimizing Programs for Fast Verification . In Proceedings of the 14th Workshop on Hot Topics in Operating Systems (HotOS). Santa Ana Pueblo, NM, 6. Jonas Wagner, Volodymyr Kuznetsov, and George Candea. 2013. -Overify: Optimizing Programs for Fast Verification. In Proceedings of the 14th Workshop on Hot Topics in Operating Systems (HotOS). Santa Ana Pueblo, NM, 6."},{"key":"e_1_3_2_1_83_1","volume-title":"Proceedings of the 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Wang Xi","year":"2014","unstructured":"Xi Wang , David Lazar , Nickolai Zeldovich , Adam Chlipala , and Zachary Tatlock . 2014 . Jitk: A Trustworthy In-Kernel Interpreter Infrastructure . In Proceedings of the 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI) . Broomfield, CO, 33--47. Xi Wang, David Lazar, Nickolai Zeldovich, Adam Chlipala, and Zachary Tatlock. 2014. Jitk: A Trustworthy In-Kernel Interpreter Infrastructure. In Proceedings of the 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI). Broomfield, CO, 33--47."},{"key":"e_1_3_2_1_84_1","doi-asserted-by":"publisher","DOI":"10.1145\/2517349.2522728"},{"key":"e_1_3_2_1_85_1","unstructured":"Andrew Waterman and Krste Asanovi\u0107 (Eds.). 2019. The RISC-V Instruction Set Manual Volume II: Privileged Architecture. RISC-V Foundation.  Andrew Waterman and Krste Asanovi\u0107 (Eds.). 2019. The RISC-V Instruction Set Manual Volume II: Privileged Architecture. RISC-V Foundation."},{"key":"e_1_3_2_1_86_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110269"},{"key":"e_1_3_2_1_87_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806610"},{"key":"e_1_3_2_1_88_1","doi-asserted-by":"publisher","DOI":"10.1145\/2043556.2043576"}],"event":{"name":"SOSP '19: ACM SIGOPS 27th Symposium on Operating Systems Principles","location":"Huntsville Ontario Canada","acronym":"SOSP '19","sponsor":["SIGOPS ACM Special Interest Group on Operating Systems","USENIX Assoc USENIX Assoc"]},"container-title":["Proceedings of the 27th ACM Symposium on Operating Systems Principles"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3341301.3359641","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3341301.3359641","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:12:56Z","timestamp":1750201976000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3341301.3359641"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,10,27]]},"references-count":86,"alternative-id":["10.1145\/3341301.3359641","10.1145\/3341301"],"URL":"https:\/\/doi.org\/10.1145\/3341301.3359641","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"}}]}}