{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T20:15:59Z","timestamp":1784232959139,"version":"3.55.0"},"publisher-location":"New York, NY, USA","reference-count":68,"publisher":"ACM","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,11,19]]},"DOI":"10.1145\/3719027.3765104","type":"proceedings-article","created":{"date-parts":[[2025,11,22]],"date-time":"2025-11-22T23:32:38Z","timestamp":1763854358000},"page":"1469-1483","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Protocols to Code: Formal Verification of a Secure Next-Generation Internet Router"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4671-4132","authenticated-orcid":false,"given":"Jo\u00e3o","family":"Pereira","sequence":"first","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6505-3942","authenticated-orcid":false,"given":"Tobias","family":"Klenze","sequence":"additional","affiliation":[{"name":"Category Labs, New York, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-9628-0007","authenticated-orcid":false,"given":"Sofia","family":"Giampietro","sequence":"additional","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0007-2805-6945","authenticated-orcid":false,"given":"Markus","family":"Limbeck","sequence":"additional","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2019-3319","authenticated-orcid":false,"given":"Dionysios","family":"Spiliopoulos","sequence":"additional","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8573-2387","authenticated-orcid":false,"given":"Felix","family":"Wolf","sequence":"additional","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4891-6950","authenticated-orcid":false,"given":"Marco","family":"Eilers","sequence":"additional","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2941-5165","authenticated-orcid":false,"given":"Christoph","family":"Sprenger","sequence":"additional","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2952-939X","authenticated-orcid":false,"given":"David","family":"Basin","sequence":"additional","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7001-2566","authenticated-orcid":false,"given":"Peter","family":"M\u00fcller","sequence":"additional","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5280-5412","authenticated-orcid":false,"given":"Adrian","family":"Perrig","sequence":"additional","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,11,22]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","unstructured":"[n.d.]. https:\/\/doi.org\/10.5281\/zenodo.16891069.","DOI":"10.5281\/zenodo.16891069"},{"key":"e_1_3_2_1_2_1","unstructured":"Prometheus Authors 2014--2024. [n.d.]. Prometheus Go client library. https: \/\/github.com\/prometheus\/client_golang\/."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/1226644.1226646"},{"key":"e_1_3_2_1_4_1","volume-title":"The Existence of Refinement Mappings. Theor. Comput. Sci. 82, 2","author":"Abadi Mart\u00edn","year":"1991","unstructured":"Mart\u00edn Abadi and Leslie Lamport. 1991. The Existence of Refinement Mappings. Theor. Comput. Sci. 82, 2 (1991)."},{"key":"e_1_3_2_1_5_1","volume-title":"Proceedings (Lecture Notes in Computer Science","volume":"63","author":"Arnaud Mathilde","year":"2011","unstructured":"Mathilde Arnaud, V\u00e9ronique Cortier, and St\u00e9phanie Delaune. 2011. Deciding Security for Protocols with Recursive Tests. In Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31 - August 5, 2011. Proceedings (Lecture Notes in Computer Science, Vol. 6803), Nikolaj Bj\u00f8rner and Viorica Sofronie-Stokkermans (Eds.). Springer, 49--63."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2014.07.004"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3576915.3623105"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP46215.2023.10179325"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3098822.3098834"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/EuroSP51992.2021.00042"},{"key":"e_1_3_2_1_11_1","volume-title":"Implementing TLS with Verified Cryptographic Security. In 2013 IEEE Symposium on Security and Privacy, SP 2013","author":"Bhargavan Karthikeyan","year":"2013","unstructured":"Karthikeyan Bhargavan, C\u00e9dric Fournet, Markulf Kohlweiss, Alfredo Pironti, and Pierre-Yves Strub. 2013. Implementing TLS with Verified Cryptographic Security. In 2013 IEEE Symposium on Security and Privacy, SP 2013, Berkeley, CA, USA, May 19--22, 2013. IEEE Computer Society, 445--459."},{"key":"e_1_3_2_1_12_1","volume-title":"An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. In 14th IEEE Computer Security Foundations Workshop (CSFW-14 2001)","author":"Blanchet Bruno","year":"2001","unstructured":"Bruno Blanchet. 2001. An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. In 14th IEEE Computer Security Foundations Workshop (CSFW-14 2001), 2001, Canada. IEEE Computer Society, 82--96."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10082-1_3"},{"key":"e_1_3_2_1_14_1","volume-title":"10th International Symposium, SAS 2003, 2003, Proceedings (Lecture Notes in Computer Science","volume":"72","author":"Boyland John","year":"2003","unstructured":"John Boyland. 2003. Checking Interference with Fractional Permissions. In Static Analysis, 10th International Symposium, SAS 2003, 2003, Proceedings (Lecture Notes in Computer Science, Vol. 2694), Radhia Cousot (Ed.). Springer, 55--72."},{"key":"e_1_3_2_1_15_1","volume-title":"A Program Logic for Verifying Secure Routing Protocols. Logical Methods in Computer Science 11, 4","author":"Chen Chen","year":"2015","unstructured":"Chen Chen, Limin Jia, Hao Xu, Cheng Luo, Wenchao Zhou, and Boon Thau Loo. 2015. A Program Logic for Verifying Secure Routing Protocols. Logical Methods in Computer Science 11, 4 (2015)."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-05288-0"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978--3-031--13188--2_7"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2017.58"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00039"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1983.1056650"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"crossref","unstructured":"Marco Eilers Malte Schwerhoff and Peter M\u00fcller. 2024. Verification Algorithms for Automated Separation Logic Verifiers. In Computer Aided Verification Arie Gurfinkel and Vijay Ganesh (Eds.). Springer Nature Switzerland Cham 362--386.","DOI":"10.1007\/978-3-031-65627-9_18"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2012.01.002"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485983.3494871"},{"key":"e_1_3_2_1_24_1","unstructured":"Google. [n.d.]. GoPacket. https:\/\/github.com\/google\/gopacket."},{"key":"e_1_3_2_1_25_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. USENIX Association, 653--669."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815428"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_3_2_1_28_1","first-page":"15","article-title":"VeriFlow: Verifying Network-Wide Invariants in Real Time","volume":"2013","author":"Khurshid Ahmed","year":"2013","unstructured":"Ahmed Khurshid, Xuan Zou, Wenxuan Zhou, Matthew Caesar, and Philip Brighten Godfrey. 2013. VeriFlow: Verifying Network-Wide Invariants in Real Time. In NSDI 2013. 15--27.","journal-title":"NSDI"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_3_2_1_30_1","volume-title":"IsaNet: Formalization of a Verification Framework for Secure Data Plane Protocols. Archive of Formal Proofs (June","author":"Klenze Tobias","year":"2022","unstructured":"Tobias Klenze and Christoph Sprenger. 2022. IsaNet: Formalization of a Verification Framework for Secure Data Plane Protocols. Archive of Formal Proofs (June 2022). https:\/\/isa-afp.org\/entries\/IsaNet.html, Formal proof development."},{"key":"e_1_3_2_1_31_1","volume-title":"Formal Verification of Secure Forwarding Protocols. In 2021 IEEE 34rd Computer Security Foundations Symposium (CSF). IEEE.","author":"Klenze Tobias","year":"2021","unstructured":"Tobias Klenze, Christoph Sprenger, and David Basin. 2021. Formal Verification of Secure Forwarding Protocols. In 2021 IEEE 34rd Computer Security Foundations Symposium (CSF). IEEE."},{"key":"e_1_3_2_1_32_1","volume-title":"IsaNet: A framework for verifying secure data plane protocols. Journal of Computer Security","author":"Klenze Tobias","year":"2022","unstructured":"Tobias Klenze, Christoph Sprenger, and David Basin. 2022. IsaNet: A framework for verifying secure data plane protocols. Journal of Computer Security (2022)."},{"key":"e_1_3_2_1_33_1","volume-title":"APLAS","author":"Kozen Dexter","year":"2014","unstructured":"Dexter Kozen. 2014. NetKAT -- A Formal System for the Verification of Networks. In Programming Languages and Systems - 12th Asian Symposium, APLAS 2014. 1--18."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535841"},{"key":"e_1_3_2_1_35_1","volume-title":"Dafny: An Automatic Program Verifier for Functional Correctness. In Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), Edmund M","author":"Leino K. Rustan M.","year":"2010","unstructured":"K. Rustan M. Leino. 2010. Dafny: An Automatic Program Verifier for Functional Correctness. In Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), Edmund M. Clarke and Andrei Voronkov (Eds.), Vol. 6355. Springer."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837622"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3230543.3230582"},{"key":"e_1_3_2_1_39_1","volume-title":"Vaandrager","author":"Lynch Nancy A.","year":"1995","unstructured":"Nancy A. Lynch and Frits W. Vaandrager. 1995. Forward and Backward Simulations: I. Untimed Systems. Inf. Comput. 121, 2 (1995)."},{"key":"e_1_3_2_1_40_1","volume-title":"CAV 2013, 2013. Proceedings (Lecture Notes in Computer Science","volume":"701","author":"Meier Simon","unstructured":"Simon Meier, Benedikt Schmidt, Cas Cremers, and David A. Basin. 2013. The TAMARIN Prover for the Symbolic Analysis of Security Protocols. In Computer Aided Verification - 25th International Conference, CAV 2013, 2013. Proceedings (Lecture Notes in Computer Science, Vol. 8044). Springer, 696--701."},{"key":"e_1_3_2_1_41_1","volume-title":"CAV 2016, Proceedings, Part I (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, Proceedings, Part I (Lecture Notes in Computer Science, Vol. 9779). Springer, 405--425."},{"key":"e_1_3_2_1_42_1","volume-title":"VMCAI 2016. Proceedings.","author":"M\u00fcller Peter","unstructured":"Peter M\u00fcller, Malte Schwerhoff, and Alexander J. Summers. 2016. Viper: A Verification Infrastructure for Permission-Based Reasoning. In Verification, Model Checking, and Abstract Interpretation - 17th International Conference, VMCAI 2016. Proceedings."},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"crossref","unstructured":"Tobias Nipkow Lawrence C. Paulson and Markus Wenzel. 2002. Isabelle\/HOL - A Proof Assistant for Higher-Order Logic. Vol. 2283. Springer.","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_3_2_1_44_1","first-page":"1","article-title":"Resources, concurrency, and local reasoning","volume":"375","author":"O'Hearn Peter W.","year":"2007","unstructured":"Peter W. O'Hearn. 2007. Resources, concurrency, and local reasoning. Theor. Comput. Sci. 375, 1--3 (2007), 271--307.","journal-title":"Theor. Comput. Sci."},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44802-0_1"},{"key":"e_1_3_2_1_46_1","volume-title":"ESOP 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, 2015. Proceedings, Jan Vitek (Ed.)","volume":"9032","author":"Penninckx Willem","year":"2015","unstructured":"Willem Penninckx, Bart Jacobs, and Frank Piessens. 2015. Sound, Modular and Compositional Verification of the Input\/Output Behavior of Programs. In Programming Languages and Systems - 24th European Symposium on Programming, ESOP 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, 2015. Proceedings, Jan Vitek (Ed.), Vol. 9032. Springer."},{"key":"e_1_3_2_1_47_1","volume-title":"Automated Verification of Network Function Binaries. In 19th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2022","author":"Pirelli Solal","year":"2022","unstructured":"Solal Pirelli, Akvile Valentukonyte, Katerina J. Argyraki, and George Candea. 2022. Automated Verification of Network Function Binaries. In 19th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2022, 2022, Amar Phanishayee and Vyas Sekar (Eds.). USENIX Association."},{"key":"e_1_3_2_1_48_1","volume-title":"Cross-Platform Cryptographic Provider. In 2020 IEEE Symposium on Security and Privacy, SP 2020","author":"Protzenko Jonathan","year":"2020","unstructured":"Jonathan Protzenko, Bryan Parno, Aymeric Fromherz, Chris Hawblitzel, Marina Polubelova, Karthikeyan Bhargavan, Benjamin Beurdouche, Joonwon Choi, Antoine Delignat-Lavaud, C\u00e9dric Fournet, Natalia Kulatova, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Christoph M. Wintersteiger, and Santiago Zanella B\u00e9guelin. 2020. EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider. In 2020 IEEE Symposium on Security and Privacy, SP 2020, 2020. IEEE."},{"key":"e_1_3_2_1_49_1","volume-title":"Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella B\u00e9guelin, Antoine Delignat-Lavaud, Catalin Hritcu, Karthikeyan Bhargavan, C\u00e9dric Fournet, and Nikhil Swamy.","author":"Protzenko Jonathan","year":"2017","unstructured":"Jonathan Protzenko, Jean Karim Zinzindohou\u00e9, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella B\u00e9guelin, Antoine Delignat-Lavaud, Catalin Hritcu, Karthikeyan Bhargavan, C\u00e9dric Fournet, and Nikhil Swamy. 2017. Verified low-level programming embedded in F. PACMPL 1, ICFP (2017)."},{"key":"e_1_3_2_1_50_1","volume-title":"ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Proceedings, Amal Ahmed (Ed.)","volume":"10801","author":"Rahli Vincent","year":"2018","unstructured":"Vincent Rahli, Ivana Vukotic, Marcus V\u00f6lp, and Paulo Jorge Esteves Ver\u00edssimo. 2018. Velisarios: Byzantine Fault-Tolerant Protocols Powered by Coq. In Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Proceedings, Amal Ahmed (Ed.), Vol. 10801. Springer."},{"key":"e_1_3_2_1_51_1","volume-title":"Separation Logic: A Logic for Shared Mutable Data Structures","author":"Reynolds John C.","year":"2002","unstructured":"John C. Reynolds. 2002. Separation Logic: A Logic for Shared Mutable Data Structures. In LICS. IEEE Computer Society, 55--74."},{"key":"e_1_3_2_1_52_1","volume-title":"Automated Analysis of Diffie-Hellman Protocols and Advanced Security Properties. In 25th IEEE Computer Security Foundations Symposium, CSF 2012","author":"Schmidt Benedikt","year":"2012","unstructured":"Benedikt Schmidt, Simon Meier, Cas J. F. Cremers, and David A. Basin. 2012. Automated Analysis of Diffie-Hellman Protocols and Advanced Security Properties. In 25th IEEE Computer Security Foundations Symposium, CSF 2012, Cambridge, MA, USA, June 25--27, 2012, Stephen Chong (Ed.). IEEE Computer Society, 78--94."},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ECOOP.2015.614"},{"key":"e_1_3_2_1_54_1","unstructured":"SIX. [n.d.]. Secure Swiss Finance Network. https:\/\/www.six-group.com\/en\/ products-services\/banking-services\/ssfn.html"},{"key":"e_1_3_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03013-0_8"},{"key":"e_1_3_2_1_56_1","volume-title":"Proc. ACM Program. Lang. 4, OOPSLA","author":"Sprenger Christoph","year":"2020","unstructured":"Christoph Sprenger, Tobias Klenze, Marco Eilers, Felix A. Wolf, Peter M\u00fcller, Martin Clochard, and David A. Basin. 2020. Igloo: soundly linking compositional refinement and separation logic for distributed system verification. Proc. ACM Program. Lang. 4, OOPSLA (2020), 152:1--152:31."},{"key":"e_1_3_2_1_57_1","volume-title":"Anvil: Verifying Liveness of Cluster Management Controllers. In 18th USENIX Symposium on Operating Systems Design and Implementation (OSDI 24)","author":"Sun Xudong","year":"2024","unstructured":"Xudong Sun, Wenjie Ma, Jiawei Tyler Gu, Zicheng Ma, Tej Chajed, Jon Howell, Andrea Lattuada, Oded Padon, Lalith Suresh, Adriana Szekeres, and Tianyin Xu. 2024. Anvil: Verifying Liveness of Cluster Management Controllers. In 18th USENIX Symposium on Operating Systems Design and Implementation (OSDI 24). USENIX Association, Santa Clara, CA, 649--666."},{"key":"e_1_3_2_1_58_1","volume-title":"The impossibility of computationally sound XOR. IACR Cryptology ePrint Archive 2010 (12","author":"Unruh Dominique","year":"2010","unstructured":"Dominique Unruh. 2010. The impossibility of computationally sound XOR. IACR Cryptology ePrint Archive 2010 (12 2010), 389."},{"key":"e_1_3_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2984012"},{"key":"e_1_3_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737958"},{"key":"e_1_3_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/3718958.3750532"},{"key":"e_1_3_2_1_62_1","volume-title":"Jo\u00e3o Carlos Pereira, and Peter M\u00fcller","author":"Wolf Felix A.","year":"2021","unstructured":"Felix A. Wolf, Linard Arquint, Martin Clochard, Wytse Oortwijn, Jo\u00e3o Carlos Pereira, and Peter M\u00fcller. 2021. Gobra: Modular Specification and Verification of Go Programs. In CAV (1) (Lecture Notes in Computer Science, Vol. 12759). Springer, 367--379."},{"key":"e_1_3_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/2854065.2854081"},{"key":"e_1_3_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359647"},{"key":"e_1_3_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/3098822.3098833"},{"key":"e_1_3_2_1_66_1","volume-title":"Automated Verification of Customizable Middlebox Properties with Gravel. In 17th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2020","author":"Zhang Kaiyuan","year":"2020","unstructured":"Kaiyuan Zhang, Danyang Zhuo, Aditya Akella, Arvind Krishnamurthy, and Xi Wang. 2020. Automated Verification of Customizable Middlebox Properties with Gravel. In 17th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2020, 2020. USENIX Association, 221--239."},{"key":"e_1_3_2_1_67_1","volume-title":"Proceedings of the Formal Methods in Computer-Aided Design (FMCAD) Conference.","author":"Zhou Yi","year":"2024","unstructured":"Yi Zhou, Jay Bosamiya, Jessica Li, Marijn Heule, and Bryan Parno. 2024. Context Pruning for More Robust SMT-based Program Verification. In Proceedings of the Formal Methods in Computer-Aided Design (FMCAD) Conference."},{"key":"e_1_3_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134043"}],"event":{"name":"CCS '25: ACM SIGSAC Conference on Computer and Communications Security","location":"Taipei Taiwan","acronym":"CCS '25","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control"]},"container-title":["Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3719027.3765104","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,12,22]],"date-time":"2025-12-22T22:14:07Z","timestamp":1766441647000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3719027.3765104"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,19]]},"references-count":68,"alternative-id":["10.1145\/3719027.3765104","10.1145\/3719027"],"URL":"https:\/\/doi.org\/10.1145\/3719027.3765104","relation":{},"subject":[],"published":{"date-parts":[[2025,11,19]]},"assertion":[{"value":"2025-11-22","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}