{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:11:56Z","timestamp":1775873516340,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":53,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,6,8]],"date-time":"2019-06-08T00:00:00Z","timestamp":1559952000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100006099","name":"Tel Aviv University","doi-asserted-by":"publisher","award":["Len Blavatnik and the Blavatnik Family foundation, Blavatnik Interdisciplinary Cyber Research Center at Tel Aviv University"],"award-info":[{"award-number":["Len Blavatnik and the Blavatnik Family foundation, Blavatnik Interdisciplinary Cyber Research Center at Tel Aviv University"]}],"id":[{"id":"10.13039\/501100006099","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001742","name":"United States - Israel Binational Science Foundation","doi-asserted-by":"publisher","award":["2016260"],"award-info":[{"award-number":["2016260"]}],"id":[{"id":"10.13039\/501100001742","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1528153,1817204"],"award-info":[{"award-number":["1528153,1817204"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100003977","name":"Israel Science Foundation","doi-asserted-by":"publisher","award":["1810\/18,1996\/18"],"award-info":[{"award-number":["1810\/18,1996\/18"]}],"id":[{"id":"10.13039\/501100003977","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Natural Sciences and Engineering Research Council of Canada"},{"DOI":"10.13039\/501100009327","name":"PAZY Foundation","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100009327","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100007297","name":"Office of Naval Research","doi-asserted-by":"publisher","award":["N68335-17-C-0558"],"award-info":[{"award-number":["N68335-17-C-0558"]}],"id":[{"id":"10.13039\/100007297","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2019,6,8]]},"DOI":"10.1145\/3314221.3314590","type":"proceedings-article","created":{"date-parts":[[2019,6,7]],"date-time":"2019-06-07T21:02:18Z","timestamp":1559941338000},"page":"1069-1084","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":71,"title":["Simple and precise static analysis of untrusted Linux kernel extensions"],"prefix":"10.1145","author":[{"given":"Elazar","family":"Gershuni","sequence":"first","affiliation":[{"name":"VMware, USA \/ Tel Aviv University, Israel"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nadav","family":"Amit","sequence":"additional","affiliation":[{"name":"VMware, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Arie","family":"Gurfinkel","sequence":"additional","affiliation":[{"name":"University of Waterloo, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nina","family":"Narodytska","sequence":"additional","affiliation":[{"name":"VMware, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jorge A.","family":"Navas","sequence":"additional","affiliation":[{"name":"SRI International, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Noam","family":"Rinetzky","sequence":"additional","affiliation":[{"name":"Tel Aviv University, Israel"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Leonid","family":"Ryzhyk","sequence":"additional","affiliation":[{"name":"VMware, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mooly","family":"Sagiv","sequence":"additional","affiliation":[{"name":"Tel Aviv University, Israel"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2019,6,8]]},"reference":[{"key":"e_1_3_2_2_1_1","volume-title":"https:\/\/github.com\/cilium\/cilium\/blob\/master\/bpf\/lxc_config.h","year":"2018","unstructured":"2018. ( 2018 ). https:\/\/github.com\/cilium\/cilium\/blob\/master\/bpf\/lxc_config.h . 2018. (2018). https:\/\/github.com\/cilium\/cilium\/blob\/master\/bpf\/lxc_config.h."},{"key":"e_1_3_2_2_2_1","volume-title":"https:\/\/github.com\/cilium\/cilium\/commit\/06efc2","year":"2018","unstructured":"2018. ( 2018 ). https:\/\/github.com\/cilium\/cilium\/commit\/06efc2 . 2018. (2018). https:\/\/github.com\/cilium\/cilium\/commit\/06efc2."},{"key":"e_1_3_2_2_3_1","unstructured":"2018. Cilium: API-aware Networking and Security. https:\/\/cilium.io\/. (2018).  2018. Cilium: API-aware Networking and Security. https:\/\/cilium.io\/. (2018)."},{"key":"e_1_3_2_2_4_1","unstructured":"2018. Coverity Scan: Linux. https:\/\/scan.coverity.com\/projects\/linux. (2018).  2018. Coverity Scan: Linux. https:\/\/scan.coverity.com\/projects\/linux. (2018)."},{"key":"e_1_3_2_2_5_1","unstructured":"2018. eBPF maps. https:\/\/prototype-kernel.readthedocs.io\/en\/latest\/bpf\/ebpf_maps.html. (2018).  2018. eBPF maps. https:\/\/prototype-kernel.readthedocs.io\/en\/latest\/bpf\/ebpf_maps.html. (2018)."},{"key":"e_1_3_2_2_6_1","unstructured":"2018. eXpress Data Path. https:\/\/prototype-kernel.readthedocs.io\/en\/latest\/networking\/XDP\/index.html. (2018).  2018. eXpress Data Path. https:\/\/prototype-kernel.readthedocs.io\/en\/latest\/networking\/XDP\/index.html. (2018)."},{"key":"e_1_3_2_2_7_1","unstructured":"2018. The extended Berkeley Packet Filter (eBPF) backend. http:\/\/llvm.org\/docs\/CodeGenerator.html#the-extended-berkeley-packet-filter-ebpf-backend. (2018).  2018. The extended Berkeley Packet Filter (eBPF) backend. http:\/\/llvm.org\/docs\/CodeGenerator.html#the-extended-berkeley-packet-filter-ebpf-backend. (2018)."},{"key":"e_1_3_2_2_8_1","unstructured":"2018. IO Visor Project. https:\/\/www.iovisor.org\/technology\/bcc. (2018).  2018. IO Visor Project. https:\/\/www.iovisor.org\/technology\/bcc. (2018)."},{"key":"e_1_3_2_2_9_1","unstructured":"2018. Production Quality Multilayer Open Virtual Switch. https:\/\/www.openvswitch.org\/. (2018).  2018. Production Quality Multilayer Open Virtual Switch. https:\/\/www.openvswitch.org\/. (2018)."},{"key":"e_1_3_2_2_10_1","unstructured":"2018. A seccomp overview. https:\/\/lwn.net\/Articles\/656307\/. (2018).  2018. A seccomp overview. https:\/\/lwn.net\/Articles\/656307\/. (2018)."},{"key":"e_1_3_2_2_11_1","unstructured":"2018. Suricata: Next Generation Intrusion Detection and Prevention Tool. https:\/\/suricata.readthedocs.io\/. (2018).  2018. Suricata: Next Generation Intrusion Detection and Prevention Tool. https:\/\/suricata.readthedocs.io\/. (2018)."},{"key":"e_1_3_2_2_12_1","unstructured":"2019. eBPF Benchmarks. (2019). https:\/\/github.com\/vbpf\/ebpf-samples.  2019. eBPF Benchmarks. (2019). https:\/\/github.com\/vbpf\/ebpf-samples."},{"key":"e_1_3_2_2_13_1","unstructured":"2019. PREVAIL: a Polynomial-Runtime EBPF Verifier using an Abstract Interpretation Layer. (2019). https:\/\/github.com\/vbpf\/ebpf-verifier.  2019. PREVAIL: a Polynomial-Runtime EBPF Verifier using an Abstract Interpretation Layer. (2019). https:\/\/github.com\/vbpf\/ebpf-verifier."},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3102980.3102987"},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3102980.3103006"},{"key":"e_1_3_2_2_16_1","first-page":"73","volume-title":"Thorough Static Analysis of Device Drivers. In European Conference on Computer Systems 2006 (EuroSys '06)","author":"Ball Thomas","year":"2006","unstructured":"Thomas Ball , Ella Bounimova , Byron Cook , Vladimir Levin , Jakob Lichtenberg , Con McGarvey , Bohus Ondrusek , Sriram K. Rajamani , and Abdullah Ustuner . 2006 . Thorough Static Analysis of Device Drivers. In European Conference on Computer Systems 2006 (EuroSys '06) . 73 - 85 . Thomas Ball, Ella Bounimova, Byron Cook, Vladimir Levin, Jakob Lichtenberg, Con McGarvey, Bohus Ondrusek, Sriram K. Rajamani, and Abdullah Ustuner. 2006. Thorough Static Analysis of Device Drivers. In European Conference on Computer Systems 2006 (EuroSys '06). 73-85."},{"key":"e_1_3_2_2_17_1","first-page":"267","volume-title":"Extensibility Safety and Performance in the SPIN Operating System. In Fifteenth ACM Symposium on Operating Systems Principles (SOSP '95)","author":"Bershad B. N.","unstructured":"B. N. Bershad , S. Savage , P. Pardyak , E. G. Sirer , M. E. Fiuczynski , D. Becker , C. Chambers , and S. Eggers . 1995 . Extensibility Safety and Performance in the SPIN Operating System. In Fifteenth ACM Symposium on Operating Systems Principles (SOSP '95) . 267 - 283 . B. N. Bershad, S. Savage, P. Pardyak, E. G. Sirer, M. E. Fiuczynski, D. Becker, C. Chambers, and S. Eggers. 1995. Extensibility Safety and Performance in the SPIN Operating System. In Fifteenth ACM Symposium on Operating Systems Principles (SOSP '95). 267-283."},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/781131.781153"},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1950365.1950396"},{"key":"e_1_3_2_2_20_1","unstructured":"Jonathan Corbet. 2018. Bounded loops in BPF programs. https:\/\/lwn.net\/Articles\/773605\/. (2018).  Jonathan Corbet. 2018. Bounded loops in BPF programs. https:\/\/lwn.net\/Articles\/773605\/. (2018)."},{"key":"e_1_3_2_2_21_1","volume-title":"Proceedings of the second international symposium on Programming","author":"Cousot Patrick","year":"1976","unstructured":"Patrick Cousot and Radhia Cousot . 1976 . Static Determination of Dynamic Properties of Programs . In Proceedings of the second international symposium on Programming , Paris, France. 106-130. Patrick Cousot and Radhia Cousot. 1976. Static Determination of Dynamic Properties of Programs. In Proceedings of the second international symposium on Programming, Paris, France. 106-130."},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-009-0089-6"},{"key":"e_1_3_2_2_24_1","volume-title":"Proceedings of the Fifth ACM Symposium on Principles of Programming Languages. 84-97","author":"Cousot Patrick","year":"1978","unstructured":"Patrick Cousot and Nicolas Halbwachs . 1978 . Automatic Discovery of Linear Constraints among Variables of a Program . In Proceedings of the Fifth ACM Symposium on Principles of Programming Languages. 84-97 . Patrick Cousot and Nicolas Halbwachs. 1978. Automatic Discovery of Linear Constraints among Variables of a Program. In Proceedings of the Fifth ACM Symposium on Principles of Programming Languages. 84-97."},{"key":"e_1_3_2_2_25_1","volume-title":"8th International Symposium, SAS 2001, Paris, France, July 16-18, 2001, Proceedings. 194-212","author":"Dor Nurit","year":"2001","unstructured":"Nurit Dor , Michael Rodeh , and Shmuel Sagiv . 2001 . Cleanness Checking of String Manipulations in C Programs via Integer Analysis. In Static Analysis , 8th International Symposium, SAS 2001, Paris, France, July 16-18, 2001, Proceedings. 194-212 . Nurit Dor, Michael Rodeh, and Shmuel Sagiv. 2001. Cleanness Checking of String Manipulations in C Programs via Integer Analysis. In Static Analysis, 8th International Symposium, SAS 2001, Paris, France, July 16-18, 2001, Proceedings. 194-212."},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/781131.781149"},{"key":"e_1_3_2_2_27_1","first-page":"177","volume-title":"Language Support for Fast and Reliable Message-based Communication in Singularity OS. In European Conference on Computer Systems 2006 (EuroSys '06)","author":"F\u00e4hndrich Manuel","year":"2006","unstructured":"Manuel F\u00e4hndrich , Mark Aiken , Chris Hawblitzel , Orion Hodson , Galen Hunt , James R. Larus , and Steven Levi . 2006 . Language Support for Fast and Reliable Message-based Communication in Singularity OS. In European Conference on Computer Systems 2006 (EuroSys '06) . 177 - 190 . Manuel F\u00e4hndrich, Mark Aiken, Chris Hawblitzel, Orion Hodson, Galen Hunt, James R. Larus, and Steven Levi. 2006. Language Support for Fast and Reliable Message-based Communication in Singularity OS. In European Conference on Computer Systems 2006 (EuroSys '06). 177-190."},{"key":"e_1_3_2_2_28_1","unstructured":"John Fastabend. 2018. [RFC PATCH 00\/16] bpf bounded loop support work in progress. https:\/\/lwn.net\/ml\/netdev\/20180601092646.15353.28269.stgit@john-Precision-Tower-5810\/. (2018).  John Fastabend. 2018. [RFC PATCH 00\/16] bpf bounded loop support work in progress. https:\/\/lwn.net\/ml\/netdev\/20180601092646.15353.28269.stgit@john-Precision-Tower-5810\/. (2018)."},{"key":"e_1_3_2_2_29_1","volume-title":"SAS 2016, Edinburgh, UK, September 8-10, 2016, Proceedings. 189-211","author":"Gange Graeme","unstructured":"Graeme Gange , Jorge A. Navas , Peter Schachte , Harald S\u00f8ndergaard , and Peter J. Stuckey . 2016. Exploiting Sparsity in Difference-Bound Matrices. In Static Analysis - 23rd International Symposium , SAS 2016, Edinburgh, UK, September 8-10, 2016, Proceedings. 189-211 . Graeme Gange, Jorge A. Navas, Peter Schachte, Harald S\u00f8ndergaard, and Peter J. Stuckey. 2016. Exploiting Sparsity in Difference-Bound Matrices. In Static Analysis - 23rd International Symposium, SAS 2016, Edinburgh, UK, September 8-10, 2016, Proceedings. 189-211."},{"key":"e_1_3_2_2_30_1","volume-title":"CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I. 343-361","author":"Gurfinkel Arie","unstructured":"Arie Gurfinkel , Temesghen Kahsai , Anvesh Komuravelli , and Jorge A. Navas . 2015. The SeaHorn Verification Framework. In Computer Aided Verification - 27th International Conference , CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I. 343-361 . Arie Gurfinkel, Temesghen Kahsai, Anvesh Komuravelli, and Jorge A. Navas. 2015. The SeaHorn Verification Framework. In Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I. 343-361."},{"key":"e_1_3_2_2_31_1","unstructured":"Jann Horn. 2018. eBPF memory corruption bugs. https:\/\/www.openwall.com\/lists\/oss-security\/2017\/12\/21\/2. (2018).  Jann Horn. 2018. eBPF memory corruption bugs. https:\/\/www.openwall.com\/lists\/oss-security\/2017\/12\/21\/2. (2018)."},{"key":"e_1_3_2_2_32_1","first-page":"661","volume-title":"Bouajjani and O. Maler (Eds.)","volume":"5643","author":"Jeannet Bertrand","year":"2009","unstructured":"Bertrand Jeannet and Antoine Min\u00e9 . 2009 . A Library of Numerical Abstract Domains for Static Analysis. In Computer Aided Verification, A . Bouajjani and O. Maler (Eds.) , Vol. 5643 . 661 - 667 . Bertrand Jeannet and Antoine Min\u00e9. 2009. A Library of Numerical Abstract Domains for Static Analysis. In Computer Aided Verification, A. Bouajjani and O. Maler (Eds.), Vol. 5643. 661-667."},{"key":"e_1_3_2_2_33_1","first-page":"202","volume-title":"Powering the Static Driver Verifier Using Corral. In 22Nd ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE","author":"Lal Akash","year":"2014","unstructured":"Akash Lal and Shaz Qadeer . 2014 . Powering the Static Driver Verifier Using Corral. In 22Nd ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE 2014). 202 - 212 . Akash Lal and Shaz Qadeer. 2014. Powering the Static Driver Verifier Using Corral. In 22Nd ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE 2014). 202-212."},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11390-005-0654-4"},{"key":"e_1_3_2_2_35_1","volume-title":"The BSD Packet Filter: A New Architecture for User-level Packet Capture. In USENIX","author":"McCanne Steven","year":"1993","unstructured":"Steven McCanne and Van Jacobson . 1993 . The BSD Packet Filter: A New Architecture for User-level Packet Capture. In USENIX Winter 1993 Conference (USENIX'93). Steven McCanne and Van Jacobson. 1993. The BSD Packet Filter: A New Architecture for User-level Packet Capture. In USENIX Winter 1993 Conference (USENIX'93)."},{"key":"e_1_3_2_2_36_1","volume-title":"Programs as Data Objects, Olivier Danvy and Andrzej Filinski (Eds.).","author":"Min\u00e9 Antoine","unstructured":"Antoine Min\u00e9 . 2001. A New Numerical Abstract Domain Based on Difference-Bound Matrices . In Programs as Data Objects, Olivier Danvy and Andrzej Filinski (Eds.). Vol. 2053 . 155-172. Antoine Min\u00e9. 2001. A New Numerical Abstract Domain Based on Difference-Bound Matrices. In Programs as Data Objects, Olivier Danvy and Andrzej Filinski (Eds.). Vol. 2053. 155-172."},{"key":"e_1_3_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1134650.1134659"},{"key":"e_1_3_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-006-8609-1"},{"key":"e_1_3_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1561\/2500000034"},{"key":"e_1_3_2_2_40_1","volume-title":"Jitk: A Trustworthy In-Kernel Interpreter Infrastructure.","author":"MIT.","year":"2014","unstructured":"MIT. 2014 . Jitk: A Trustworthy In-Kernel Interpreter Infrastructure. (2014). http:\/\/css.csail.mit.edu\/jitk\/. MIT. 2014. Jitk: A Trustworthy In-Kernel Interpreter Infrastructure. (2014). http:\/\/css.csail.mit.edu\/jitk\/."},{"key":"e_1_3_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2016.07.030"},{"key":"e_1_3_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1950365.1950401"},{"key":"e_1_3_2_2_43_1","volume-title":"4th International Conference, VMCAI 2003, New York, NY, USA, January 9-11, 2002, Proceedings. 41-55","author":"Rival Xavier","year":"2003","unstructured":"Xavier Rival . 2003 . Abstract Interpretation-Based Certification of Assembly Code. In Verification, Model Checking, and Abstract Interpretation , 4th International Conference, VMCAI 2003, New York, NY, USA, January 9-11, 2002, Proceedings. 41-55 . Xavier Rival. 2003. Abstract Interpretation-Based Certification of Assembly Code. In Verification, Model Checking, and Abstract Interpretation, 4th International Conference, VMCAI 2003, New York, NY, USA, January 9-11, 2002, Proceedings. 41-55."},{"key":"e_1_3_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1275497.1275501"},{"key":"e_1_3_2_2_45_1","unstructured":"Jay Schulist Daniel Borkmann and Alexei Starovoitov. 2018. Linux Socket Filtering aka Berkeley Packet Filter (BPF). https:\/\/www.kernel.org\/doc\/Documentation\/networking\/filter.txt. (2018).  Jay Schulist Daniel Borkmann and Alexei Starovoitov. 2018. Linux Socket Filtering aka Berkeley Packet Filter (BPF). https:\/\/www.kernel.org\/doc\/Documentation\/networking\/filter.txt. (2018)."},{"key":"e_1_3_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.5555\/1929820.1929822"},{"key":"e_1_3_2_2_47_1","volume-title":"9th International Conference, CC 2000, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS 2000, Berlin, Germany, Arch 25 - April 2, 2000, Proceedings. 50-66","author":"Shaham Ran","year":"2000","unstructured":"Ran Shaham , Elliot K. Kolodner , and Shmuel Sagiv . 2000 . Automatic Removal of Array Memory Leaks in Java. In Compiler Construction , 9th International Conference, CC 2000, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS 2000, Berlin, Germany, Arch 25 - April 2, 2000, Proceedings. 50-66 . Ran Shaham, Elliot K. Kolodner, and Shmuel Sagiv. 2000. Automatic Removal of Array Memory Leaks in Java. In Compiler Construction, 9th International Conference, CC 2000, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS 2000, Berlin, Germany, Arch 25 - April 2, 2000, Proceedings. 50-66."},{"key":"e_1_3_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2738000"},{"key":"e_1_3_2_2_49_1","first-page":"46","volume-title":"Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017","author":"Singh Gagandeep","year":"2017","unstructured":"Gagandeep Singh , Markus P\u00fcschel , and Martin T. Vechev . 2017. Fast polyhedra abstract domain . In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017 , Paris, France , January 18-20, 2017 . 46 - 59 . Gagandeep Singh, Markus P\u00fcschel, and Martin T. Vechev. 2017. Fast polyhedra abstract domain. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017. 46-59."},{"key":"e_1_3_2_2_50_1","volume-title":"Vechev","author":"Singh Gagandeep","year":"2018","unstructured":"Gagandeep Singh , Markus P\u00fcschel , and Martin T . Vechev . 2018 . A practical construction for decomposing numerical abstract domains. PACMPL 2, POPL ( 2018), 55:1-55:28. Gagandeep Singh, Markus P\u00fcschel, and Martin T. Vechev. 2018. A practical construction for decomposing numerical abstract domains. PACMPL 2, POPL (2018), 55:1-55:28."},{"key":"e_1_3_2_2_51_1","first-page":"207","volume-title":"Improving the Reliability of Commodity Operating Systems. In Nineteenth ACM Symposium on Operating Systems Principles (SOSP '03)","author":"Swift Michael M.","unstructured":"Michael M. Swift , Brian N. Bershad , and Henry M. Levy . 2003 . Improving the Reliability of Commodity Operating Systems. In Nineteenth ACM Symposium on Operating Systems Principles (SOSP '03) . 207 - 222 . Michael M. Swift, Brian N. Bershad, and Henry M. Levy. 2003. Improving the Reliability of Commodity Operating Systems. In Nineteenth ACM Symposium on Operating Systems Principles (SOSP '03). 207-222."},{"key":"e_1_3_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/996841.996869"},{"key":"e_1_3_2_2_53_1","first-page":"33","volume-title":"Jitk: A Trustworthy In-Kernel Interpreter Infrastructure. In 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI 14)","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 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI 14) . USENIX Association, Broomfield, CO , 33 - 47 . https:\/\/www.usenix.org\/conference\/osdi14\/technical-sessions\/presentation\/wang_xi. Xi Wang, David Lazar, Nickolai Zeldovich, Adam Chlipala, and Zachary Tatlock. 2014. Jitk: A Trustworthy In-Kernel Interpreter Infrastructure. In 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI 14). USENIX Association, Broomfield, CO, 33-47. https:\/\/www.usenix.org\/conference\/osdi14\/technical-sessions\/presentation\/wang_xi."}],"event":{"name":"PLDI '19: 40th ACM SIGPLAN Conference on Programming Language Design and Implementation","location":"Phoenix AZ USA","acronym":"PLDI '19","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3314221.3314590","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3314221.3314590","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3314221.3314590","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:53:22Z","timestamp":1750204402000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3314221.3314590"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,6,8]]},"references-count":53,"alternative-id":["10.1145\/3314221.3314590","10.1145\/3314221"],"URL":"https:\/\/doi.org\/10.1145\/3314221.3314590","relation":{},"subject":[],"published":{"date-parts":[[2019,6,8]]},"assertion":[{"value":"2019-06-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}