{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,11]],"date-time":"2026-08-11T19:28:02Z","timestamp":1786476482601,"version":"build-2736575974"},"publisher-location":"New York, NY, USA","reference-count":59,"publisher":"ACM","license":[{"start":{"date-parts":[[2026,8,11]],"date-time":"2026-08-11T00:00:00Z","timestamp":1786406400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"funder":[{"name":"New Generation Artificial Intelligence-National Science and Technology Major Project","award":["2025ZD0122102"],"award-info":[{"award-number":["2025ZD0122102"]}]},{"name":"National Natural Science Foundation of China","award":["62532010"],"award-info":[{"award-number":["62532010"]}]},{"name":"National Natural Science Foundation of China","award":["62572408"],"award-info":[{"award-number":["62572408"]}]},{"name":"Fujian Provincial Science and Technology Project","award":["2025H6021"],"award-info":[{"award-number":["2025H6021"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2026,8,17]]},"DOI":"10.1145\/3789240.3829122","type":"proceedings-article","created":{"date-parts":[[2026,8,11]],"date-time":"2026-08-11T18:33:22Z","timestamp":1786473202000},"page":"74-91","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Towards Efficient Verification of Distributed In-Network Computing Programs"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0000-9821-5031","authenticated-orcid":false,"given":"Mingyuan","family":"Song","sequence":"first","affiliation":[{"name":"Fujian Engineering Research Center of High-Performance Intelligent Computing Systems, School of Informatics, Xiamen University, Xiamen, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-5877-4882","authenticated-orcid":false,"given":"Huan","family":"Shen","sequence":"additional","affiliation":[{"name":"Fujian Engineering Research Center of High-Performance Intelligent Computing Systems, School of Informatics, Xiamen University, Xiamen, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-2842-6392","authenticated-orcid":false,"given":"Jinghui","family":"Jiang","sequence":"additional","affiliation":[{"name":"Fujian Engineering Research Center of High-Performance Intelligent Computing Systems, School of Informatics, Xiamen University, Xiamen, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4482-6248","authenticated-orcid":false,"given":"Qiang","family":"Su","sequence":"additional","affiliation":[{"name":"Fujian Engineering Research Center of High-Performance Intelligent Computing Systems, School of Informatics, Xiamen University, Xiamen, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-7268-4874","authenticated-orcid":false,"given":"Ziheng","family":"Zhang","sequence":"additional","affiliation":[{"name":"Fujian Engineering Research Center of High-Performance Intelligent Computing Systems, School of Informatics, Xiamen University, Xiamen, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-9153-467X","authenticated-orcid":false,"given":"Qingyu","family":"Song","sequence":"additional","affiliation":[{"name":"Fujian Engineering Research Center of High-Performance Intelligent Computing Systems, School of Informatics, Xiamen University, Xiamen, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0135-8915","authenticated-orcid":false,"given":"Yuchao","family":"Zhang","sequence":"additional","affiliation":[{"name":"Beijing University of Posts and Telecommunications, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-5161-5697","authenticated-orcid":false,"given":"Wanjian","family":"Feng","sequence":"additional","affiliation":[{"name":"Yealink, Xiamen, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8614-8756","authenticated-orcid":false,"given":"Fei","family":"Yuan","sequence":"additional","affiliation":[{"name":"School of Informatics, Xiamen University, Xiamen, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8123-0347","authenticated-orcid":false,"given":"Yitao","family":"Xing","sequence":"additional","affiliation":[{"name":"Huawei Technologies Co., Ltd., Shenzhen, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8336-7224","authenticated-orcid":false,"given":"Wenjia","family":"Wei","sequence":"additional","affiliation":[{"name":"Huawei Technologies Co., Ltd., Nanjing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3394-6279","authenticated-orcid":false,"given":"Qiao","family":"Xiang","sequence":"additional","affiliation":[{"name":"Fujian Engineering Research Center of High-Performance Intelligent Computing Systems, School of Informatics, Xiamen University, Xiamen, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7362-2789","authenticated-orcid":false,"given":"Jiwu","family":"Shu","sequence":"additional","affiliation":[{"name":"Fujian Engineering Research Center of High-Performance Intelligent Computing Systems, School of Informatics, Xiamen University, Xiamen, China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,8,11]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/1086.001.0001"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133934"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/TNET.2021.3113370"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2656877.2656890"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3629144"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/TNET.2020.3045293"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0058022"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/TNET.2020.2992106"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3387514.3405888"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3185467.3185499"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45190-5_4"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"crossref","unstructured":"Florian Frohn and J\u00fcrgen Giesl. 2025. Integrating Loop Acceleration Into Bounded Model Checking. In Formal Methods Andr\u00e9 Platzer Kristin Yvonne Rozier Matteo Pradella and Matteo Rossi (Eds.). Springer Nature Switzerland Cham 73\u201391.","DOI":"10.1007\/978-3-031-71162-6_4"},{"key":"e_1_3_2_1_13_1","volume-title":"Rui Miao, Yu Zhou, Bingchuan Tian, Chen Sun, Dennis Cai, Ming Zhang, and Minlan Yu.","author":"Gao Jiaqi","year":"2020","unstructured":"Jiaqi Gao, Ennan Zhai, Hongqiang Harry Liu, Rui Miao, Yu Zhou, Bingchuan Tian, Chen Sun, Dennis Cai, Ming Zhang, and Minlan Yu. 2020. Lyra: A cross-platform language and compiler for data plane programming on heterogeneous asics. In Proceedings of the Annual conference of the ACM Special Interest Group on Data Communication on the applications, technologies, architectures, and protocols for computer communication. Association for Computing Machinery, New York, NY, USA, 435\u2013450."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815428"},{"key":"e_1_3_2_1_15_1","unstructured":"Intel. 2016. Intel Tofino. https:\/\/www.intel.com\/content\/www\/us\/en\/products\/details\/network-io\/intelligent-fabric-processors\/tofino.html"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3514221.3517825"},{"key":"e_1_3_2_1_17_1","volume-title":"Reducing Write Tail Latency of Distributed Key-Value Stores Using In-Network Chasing. In 2024 IEEE\/ACM 32nd International Symposium on Quality of Service (IWQoS). IEEE, IEEE","author":"Jiang Jinghui","year":"2024","unstructured":"Jinghui Jiang, Xiwen Fan, Zhenpei Huang, Kairui Zhou, Qiao Xiang, Lu Tang, Qiang Li, and Jiwu Shu. 2024. Reducing Write Tail Latency of Distributed Key-Value Stores Using In-Network Chasing. In 2024 IEEE\/ACM 32nd International Symposium on Quality of Service (IWQoS). IEEE, IEEE, Piscataway, NJ, USA, 1\u201310."},{"key":"e_1_3_2_1_18_1","volume-title":"NetChain: Scale-Free Sub-RTT Coordination. In 15th USENIX Symposium on Networked Systems Design and Implementation (NSDI 18)","author":"Jin Xin","year":"2018","unstructured":"Xin Jin, Xiaozhou Li, Haoyu Zhang, Nate Foster, Jeongkeun Lee, Robert Soul\u00e9, Changhoon Kim, and Ion Stoica. 2018. NetChain: Scale-Free Sub-RTT Coordination. In 15th USENIX Symposium on Networked Systems Design and Implementation (NSDI 18). USENIX Association, Renton, WA, 35\u201349. https:\/\/www.usenix.org\/conference\/nsdi18\/presentation\/jin"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132764"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99527-0_35"},{"key":"e_1_3_2_1_21_1","volume-title":"19th USENIX Symposium on Networked Systems Design and Implementation (NSDI 22)","author":"Kraft Peter","year":"2022","unstructured":"Peter Kraft, Fiodar Kazhamiaka, Peter Bailis, and Matei Zaharia. 2022. {Data-Parallel} actors: A programming model for scalable query serving systems. In 19th USENIX Symposium on Networked Systems Design and Implementation (NSDI 22). USENIX Association, Berkeley, CA, USA, 1059\u20131074."},{"key":"e_1_3_2_1_22_1","volume-title":"Specifying systems: the TLA+ language and tools for hardware and software engineers","author":"Lamport Leslie","unstructured":"Leslie Lamport. 2002. Specifying systems: the TLA+ language and tools for hardware and software engineers. Addison-Wesley, Boston, MA, USA."},{"key":"e_1_3_2_1_23_1","volume-title":"18th USENIX Symposium on Networked Systems Design and Implementation (NSDI 21)","author":"Lao ChonLam","year":"2021","unstructured":"ChonLam Lao, Yanfang Le, Kshiteej Mahajan, Yixi Chen, Wenfei Wu, Aditya Akella, and Michael Swift. 2021. {ATP}: In-network aggregation for multi-tenant learning. In 18th USENIX Symposium on Networked Systems Design and Implementation (NSDI 21). USENIX Association, Berkeley, CA, USA, 741\u2013761."},{"key":"e_1_3_2_1_24_1","volume-title":"2019 IFIP\/IEEE Symposium on Integrated Network and Service Management (IM). IEEE, IEEE","author":"Lapolli \u00c2ngelo Cardoso","year":"2019","unstructured":"\u00c2ngelo Cardoso Lapolli, Jonatas Adilson Marques, and Luciano Paschoal Gaspary. 2019. Offloading real-time DDoS attack detection to programmable data planes. In 2019 IFIP\/IEEE Symposium on Integrated Network and Service Management (IM). IEEE, IEEE, Piscataway, NJ, USA, 19\u201327."},{"key":"e_1_3_2_1_25_1","volume-title":"This is Boogie 2. (June","author":"Leino K. Rustan M.","year":"2008","unstructured":"K. Rustan M. Leino. 2008. This is Boogie 2. (June 2008). https:\/\/www.microsoft.com\/en-us\/research\/publication\/this-is-boogie-2-2\/"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.14778\/3551793.3551838"},{"key":"e_1_3_2_1_27_1","volume-title":"14th USENIX Symposium on Operating Systems Design and Implementation (OSDI 20)","author":"Li Jialin","year":"2020","unstructured":"Jialin Li, Jacob Nelson, Ellis Michael, Xin Jin, and Dan RK Ports. 2020. Pegasus: Tolerating skewed workloads in distributed storage with {In-Network} coherence directories. In 14th USENIX Symposium on Operating Systems Design and Implementation (OSDI 20). USENIX Association, Berkeley, CA, USA, 387\u2013406."},{"key":"e_1_3_2_1_28_1","volume-title":"19th USENIX Symposium on Networked Systems Design and Implementation (NSDI 22)","author":"Li Yifan","year":"2022","unstructured":"Yifan Li, Jiaqi Gao, Ennan Zhai, Mengqi Liu, Kun Liu, and Hongqiang Harry Liu. 2022. Cetus: Releasing P4 Programmers from the Chore of Trial and Error Compiling. In 19th USENIX Symposium on Networked Systems Design and Implementation (NSDI 22). USENIX Association, Renton, WA, 371\u2013385. https:\/\/www.usenix.org\/conference\/nsdi22\/presentation\/li-yifan"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/INFOCOMWKSHPS50562.2020.9162975"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3230543.3230582"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3037697.3037731"},{"key":"e_1_3_2_1_32_1","volume-title":"DistCache: Provable Load Balancing for Large-Scale Storage Systems with Distributed Caching. In 17th USENIX Conference on File and Storage Technologies (FAST 19)","author":"Liu Zaoxing","year":"2019","unstructured":"Zaoxing Liu, Zhihao Bai, Zhenming Liu, Xiaozhou Li, Changhoon Kim, Vladimir Braverman, Xin Jin, and Ion Stoica. 2019. DistCache: Provable Load Balancing for Large-Scale Storage Systems with Distributed Caching. In 17th USENIX Conference on File and Storage Technologies (FAST 19). USENIX Association, Boston, MA, 143\u2013157."},{"key":"e_1_3_2_1_33_1","unstructured":"Nuno Lopes Nikolaj Bj\u00f8rner Nick McKeown Andrey Rybalchenko Dan Talayco and George Varghese. 2016. Automatically verifying reachability and wellformedness in P4 Networks. Technical Report MSR-TR-2016-65. Microsoft Research. 1\u201313 pages."},{"key":"e_1_3_2_1_34_1","unstructured":"National Vulnerability Database. 2024. CVE-2024-0106: NVIDIA ConnectX Host Firmware for BlueField DPU. https:\/\/nvd.nist.gov\/vuln\/detail\/CVE-2024-0106. NVD entry: denial of service data tampering and limited information disclosure."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3281411.3281421"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.23919\/IFIPNetworking.2019.8816830"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2901318.2901343"},{"key":"e_1_3_2_1_38_1","unstructured":"P4 Language Consortium. 2015. BMv2: The P4 Behavioral Model. https:\/\/github.com\/p4lang\/behavioral-model."},{"key":"e_1_3_2_1_39_1","unstructured":"P4 Language Consortium. 2017. p4c: The P4 Reference Compiler. https:\/\/github.com\/p4lang\/p4c."},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3603269.3604834"},{"key":"e_1_3_2_1_41_1","volume-title":"14th USENIX Symposium on Operating Systems Design and Implementation (OSDI 20)","author":"Ruffy Fabian","year":"2020","unstructured":"Fabian Ruffy, Tao Wang, and Anirudh Sivaraman. 2020. Gauntlet: Finding bugs in compilers for programmable packet processing. In 14th USENIX Symposium on Operating Systems Design and Implementation (OSDI 20). USENIX Association, Berkeley, CA, USA, 683\u2013699."},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158116"},{"key":"e_1_3_2_1_43_1","volume-title":"2023 USENIX Annual Technical Conference (USENIX ATC 23)","author":"Sheng Siyuan","year":"2023","unstructured":"Siyuan Sheng, Huancheng Puyang, Qun Huang, Lu Tang, and Patrick PC Lee. 2023. {FarReach}: Write-back Caching in Programmable Switches. In 2023 USENIX Annual Technical Conference (USENIX ATC 23). USENIX Association, Berkeley, CA, USA, 571\u2013584."},{"key":"e_1_3_2_1_44_1","volume-title":"Lark: A modern parsing library for Python. https:\/\/github.com\/lark-parser\/lark.","author":"Shinan Erez","year":"2025","unstructured":"Erez Shinan. 2025. Lark: A modern parsing library for Python. https:\/\/github.com\/lark-parser\/lark."},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3230543.3230548"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3452296.3472937"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290372"},{"key":"e_1_3_2_1_48_1","volume-title":"Concordia: Distributed Shared Memory with In-Network Cache Coherence. In 19th USENIX Conference on File and Storage Technologies, FAST 2021","author":"Wang Qing","year":"2021","unstructured":"Qing Wang, Youyou Lu, Erci Xu, Junru Li, Youmin Chen, and Jiwu Shu. 2021. Concordia: Distributed Shared Memory with In-Network Cache Coherence. In 19th USENIX Conference on File and Storage Technologies, FAST 2021, February 23\u201325, 2021. USENIX Association, Berkeley, CA, USA, 277\u2013292."},{"key":"e_1_3_2_1_49_1","first-page":"352","article-title":"Program slicing","volume":"10","author":"Weiser Mark","year":"2009","unstructured":"Mark Weiser. 2009. Program slicing. IEEE Transactions on software engineering 10, 4 (2009), 352\u2013357.","journal-title":"IEEE Transactions on software engineering"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3603269.3604835"},{"key":"e_1_3_2_1_51_1","volume-title":"21st USENIX Symposium on Networked Systems Design and Implementation (NSDI 24)","author":"Yassini Parham","year":"2024","unstructured":"Parham Yassini, Khaled Diab, Saeed Mahloujifar, and Mohamed Hefeeda. 2024. Horus: Granular {in-network} task scheduler for cloud datacenters. In 21st USENIX Symposium on Networked Systems Design and Implementation (NSDI 24). USENIX Association, Berkeley, CA, USA, 1\u201322."},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3387514.3405857"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3651890.3672213"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3422604.3425946"},{"key":"e_1_3_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1109\/INFOCOM52122.2024.10621366"},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.5555\/3767955.3767968"},{"key":"e_1_3_2_1_57_1","volume-title":"18th USENIX Symposium on Operating Systems Design and Implementation (OSDI 24)","author":"Zhang Hanze","year":"2024","unstructured":"Hanze Zhang, Ke Cheng, Rong Chen, and Haibo Chen. 2024. Fast and scalable in-network lock management using lock fission. In 18th USENIX Symposium on Operating Systems Design and Implementation (OSDI 24). USENIX Association, Berkeley, CA, USA, 251\u2013268."},{"key":"e_1_3_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/3603269.3604813"},{"key":"e_1_3_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/3544216.3544247"}],"event":{"name":"SIGCOMM '26: ACM SIGCOMM 2026 Conference","location":"Colorado Convention Center Denver CO USA","acronym":"SIGCOMM '26","sponsor":["SIGCOMM ACM Special Interest Group on Data Communication"]},"container-title":["Proceedings of the ACM SIGCOMM 2026 Conference"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3789240.3829122","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,8,11]],"date-time":"2026-08-11T18:42:30Z","timestamp":1786473750000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3789240.3829122"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,8,11]]},"references-count":59,"alternative-id":["10.1145\/3789240.3829122","10.1145\/3789240"],"URL":"https:\/\/doi.org\/10.1145\/3789240.3829122","relation":{},"subject":[],"published":{"date-parts":[[2026,8,11]]},"assertion":[{"value":"2026-08-11","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}