{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T21:34:13Z","timestamp":1781040853421,"version":"3.54.1"},"reference-count":30,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T00:00:00Z","timestamp":1748736000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0"},{"start":{"date-parts":[[2025,6,12]],"date-time":"2025-06-12T00:00:00Z","timestamp":1749686400000},"content-version":"vor","delay-in-days":11,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0"}],"funder":[{"DOI":"10.13039\/501100012165","name":"Key Technologies Research and Development Program","doi-asserted-by":"publisher","award":["2022YFB2901501"],"award-info":[{"award-number":["2022YFB2901501"]}],"id":[{"id":"10.13039\/501100012165","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J. King Saud Univ. Comput. Inf. Sci."],"published-print":{"date-parts":[[2025,6]]},"DOI":"10.1007\/s44443-025-00083-6","type":"journal-article","created":{"date-parts":[[2025,6,12]],"date-time":"2025-06-12T15:25:57Z","timestamp":1749741957000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["NetChecker: enabling real-time and error-locatable runtime verification for programmable networks"],"prefix":"10.1007","volume":"37","author":[{"given":"Ying","family":"Yao","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Le","family":"Tian","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-6522-2321","authenticated-orcid":false,"given":"Yuxiang","family":"Hu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,6,12]]},"reference":[{"key":"83_CR1","unstructured":"p4lang (2015) P4 tutorials. https:\/\/github.com\/p4lang\/tutorials, accessed on October, 2024"},{"key":"83_CR2","unstructured":"NEOAdvancedTechnology (2016) codes. https:\/\/github.com\/NEOAdvancedTechnology\/ts_switching_P4, accessed on October, 2024"},{"key":"83_CR3","doi-asserted-by":"publisher","unstructured":"Anderson CJ, Foster N, Guha A, et\u00a0al (2014) Netkat: semantic foundations for networks. In: Proceedings of the 41st ACM SIGPLAN-SIGACT symposium on principles of programming languages. association for computing machinery, New York, NY, USA, POPL \u201914, p 113\u2013126. https:\/\/doi.org\/10.1145\/2535838.2535862","DOI":"10.1145\/2535838.2535862"},{"key":"83_CR4","unstructured":"Ball T, Larus JR (1996) Efficient path profiling. In: Proceedings of the 29th Annual ACM\/IEEE international symposium on microarchitecture. IEEE Computer Society, USA, MICRO 29, pp 46\u201357"},{"key":"83_CR5","doi-asserted-by":"publisher","unstructured":"Beckett R, Zou XK, Zhang S, et\u00a0al (2014) An assertion language for debugging sdn applications. In: Proceedings of the third workshop on hot topics in software defined networking. Association for Computing Machinery, New York, NY, USA, HotSDN \u201914, pp 91\u201396. https:\/\/doi.org\/10.1145\/2620728.2620743","DOI":"10.1145\/2620728.2620743"},{"key":"83_CR6","doi-asserted-by":"publisher","unstructured":"Ben\u00a0Basat R, Ramanathan S, Li Y, et\u00a0al (2020) Pint: Probabilistic in-band network telemetry. 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, SIGCOMM \u201920, p 662\u201368https:\/\/doi.org\/10.1145\/3387514.3405894, https:\/\/doi.org\/10.1145\/3387514.3405894","DOI":"10.1145\/3387514.3405894"},{"issue":"3","key":"83_CR7","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1145\/2656877.2656890","volume":"44","author":"P Bosshart","year":"2014","unstructured":"Bosshart P, Daly D, Gibb G et al (2014) P4: programming protocol-independent packet processors. SIGCOMM Comput Commun Rev 44(3):87\u201395. https:\/\/doi.org\/10.1145\/2656877.2656890","journal-title":"SIGCOMM Comput Commun Rev"},{"key":"83_CR8","unstructured":"Canini M, Venzano D, Pere\u0161\u00edni P, et\u00a0al (2012) A nice way to test openflow applications. In: Proceedings of the 9th USENIX conference on networked systems design and implementation. USENIX Association, USA, NSDI\u201912, p\u00a010"},{"key":"83_CR9","doi-asserted-by":"publisher","unstructured":"Cantelli-Forti A, Capria A, Saverino AL et al (2021) Critical infrastructure protection system design based on scout multitech security system for interconnected space control ground stations. Int J Crit Infrastr Protect 32:100407. https:\/\/doi.org\/10.1016\/j.ijcip.2020.100407https:\/\/www.sciencedirect.com\/science\/article\/pii\/S1874548220300718","DOI":"10.1016\/j.ijcip.2020.100407"},{"key":"83_CR10","doi-asserted-by":"publisher","unstructured":"Chang Y, Jiang C, Chandra A, et\u00a0al (2019) Lancet: better network resilience by designing for pruned failure sets. Proc ACM Meas Anal Comput Syst 3(3). https:\/\/doi.org\/10.1145\/3366697","DOI":"10.1145\/3366697"},{"key":"83_CR11","unstructured":"Chang Y, Rao S, Tawarmalani M (2017) Robust validation of network designs under uncertain demands and failures. In: 14th USENIX symposium on networked systems design and implementation (NSDI 17). USENIX Association, Boston, MA, pp 347\u2013362. https:\/\/www.usenix.org\/conference\/nsdi17\/technical-sessions\/presentation\/chang"},{"key":"83_CR12","unstructured":"Edwards TG, Ciarleglio N, Networks A (2017) Timestamp-aware RTP video switching using programmable data plane. https:\/\/api.semanticscholar.org\/CorpusID:40925035"},{"key":"83_CR13","doi-asserted-by":"publisher","unstructured":"Freire L, Neves M, Leal L, et\u00a0al (2018) Uncovering bugs in p4 programs with assertion-based verification. In: Proceedings of the symposium on SDN research. Association for Computing Machinery, New York, NY, USA, SOSR \u201918. https:\/\/doi.org\/10.1145\/3185467.3185499","DOI":"10.1145\/3185467.3185499"},{"key":"83_CR14","unstructured":"Hira M, Wobker L (2015) Improving network monitoring and management with programmable data planes. 28:2021"},{"key":"83_CR15","doi-asserted-by":"publisher","unstructured":"Jiang C, Rao S, Tawarmalani M (2020) Pcf: Provably resilient flexible routing. 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, SIGCOMM \u201920, pp 139\u201315https:\/\/doi.org\/10.1145\/3387514.3405858","DOI":"10.1145\/3387514.3405858"},{"key":"83_CR16","doi-asserted-by":"crossref","unstructured":"Jin X, Li X, Zhang H, et\u00a0al (2017) Netcache: Balancing key-value stores with fast in-network caching. In: Proceedings of the 26th symposium on operating systems principles, pp 121\u2013136","DOI":"10.1145\/3132747.3132764"},{"key":"83_CR17","doi-asserted-by":"publisher","unstructured":"Kumar KS, K R, Prashanth PS, et\u00a0al (2021) Dbval: Validating p4 data plane runtime behavior. In: Proceedings of the ACM SIGCOMM symposium on SDN research (SOSR). Association for Computing Machinery, New York, NY, USA, SOSR \u201921, pp 122\u2013134. https:\/\/doi.org\/10.1145\/3482898.3483352","DOI":"10.1145\/3482898.3483352"},{"key":"83_CR18","unstructured":"Lao C, Le Y, Mahajan K, et\u00a0al (2021) ATP: In-network aggregation for multi-tenant learning. In: 18th USENIX symposium on networked systems design and implementation (NSDI 21). USENIX Association, pp 741\u2013761. https:\/\/www.usenix.org\/conference\/nsdi21\/presentation\/lao"},{"key":"83_CR19","doi-asserted-by":"publisher","unstructured":"Li Y, Miao R, Liu HH, et\u00a0al (2019) Hpcc: high precision congestion control. In: Proceedings of the ACM special interest group on data communication. Association for Computing Machinery, New York, NY, USA, SIGCOMM \u201919, p 44\u201358. https:\/\/doi.org\/10.1145\/3341302.3342085","DOI":"10.1145\/3341302.3342085"},{"key":"83_CR20","unstructured":"Lopes NP, Bj\u00f8rner N, Godefroid P, et\u00a0al (2015) Checking beliefs in dynamic networks. In: 12th USENIX symposium on networked systems design and implementation (NSDI 15), pp 499\u2013512"},{"key":"83_CR21","unstructured":"Maccioni F (2017) Network path not found? forward networks blog. https:\/\/bit.ly\/2FzpEEZ, accessed on September, 2024"},{"key":"83_CR22","unstructured":"Ruffy F, Wang T, Sivaraman A (2020) Gauntlet: Finding bugs in compilers for programmable packet processing. In: 14th USENIX symposium on operating systems design and implementation (OSDI 20). USENIX Association, pp 683\u2013699. https:\/\/www.usenix.org\/conference\/osdi20\/presentation\/ruffy"},{"issue":"7","key":"83_CR23","doi-asserted-by":"publisher","first-page":"1293","DOI":"10.1109\/JSAC.2020.2999653","volume":"38","author":"A Shukla","year":"2020","unstructured":"Shukla A, Fathalli S, Zinner T et al (2020) P4consist: toward consistent p4 sdns. IEEE J Sel Areas Commun 38(7):1293\u20131307. https:\/\/doi.org\/10.1109\/JSAC.2020.2999653","journal-title":"IEEE J Sel Areas Commun"},{"issue":"4","key":"83_CR24","doi-asserted-by":"publisher","first-page":"1822","DOI":"10.1109\/TNET.2023.3234931","volume":"31","author":"A Shukla","year":"2023","unstructured":"Shukla A, Hudemann K, V\u00e1gi Z et al (2023) Runtime verification for programmable switches. IEEE\/ACM Trans Netw 31(4):1822\u20131837. https:\/\/doi.org\/10.1109\/TNET.2023.3234931","journal-title":"IEEE\/ACM Trans Netw"},{"key":"83_CR25","doi-asserted-by":"publisher","unstructured":"Shukla A, Hudemann KN, Hecker A, et\u00a0al (2019) Runtime verification of p4 switches with reinforcement learning. In: Proceedings of the 2019 workshop on network meets AI & ML. Association for Computing Machinery, New York, NY, USA, NetAI\u201919, p 1\u20137. https:\/\/doi.org\/10.1145\/3341216.3342206","DOI":"10.1145\/3341216.3342206"},{"key":"83_CR26","doi-asserted-by":"publisher","unstructured":"Shukla A, Hudemann K, V\u00e1gi Z, et\u00a0al (2021) Fix with p6: Verifying programmable switches at runtime. In: IEEE INFOCOM 2021 - IEEE conference on computer communications. IEEE Press, pp 1\u201310. https:\/\/doi.org\/10.1109\/INFOCOM42981.2021.9488772","DOI":"10.1109\/INFOCOM42981.2021.9488772"},{"key":"83_CR27","doi-asserted-by":"publisher","unstructured":"Stoenescu R, Dumitrescu D, Popovici M, et\u00a0al (2018) Debugging p4 programs with vera. In: Proceedings of the 2018 conference of the ACM special interest group on data communication. association for computing machinery, New York, NY, USA, SIGCOMM \u201918, pp 518\u2013532. https:\/\/doi.org\/10.1145\/3230543.3230548","DOI":"10.1145\/3230543.3230548"},{"key":"83_CR28","doi-asserted-by":"crossref","unstructured":"Tian B, Gao J, Liu M, et\u00a0al (2021) Aquila: a practically usable verification system for production-scale programmable data planes. In: Proceedings of the 2021 ACM SIGCOMM 2021 conference. https:\/\/api.semanticscholar.org\/CorpusID:236209282","DOI":"10.1145\/3452296.3472937"},{"key":"83_CR29","doi-asserted-by":"publisher","unstructured":"Yang Y, He L, Zhou J, et\u00a0al (2024) P4runpro: Enabling runtime programmability for rmt programmable switches. In: Proceedings of the ACM SIGCOMM 2024 conference. association for computing machinery, New York, NY, USA, ACM SIGCOMM \u201924, p 921\u2013937. https:\/\/doi.org\/10.1145\/3651890.3672230","DOI":"10.1145\/3651890.3672230"},{"key":"83_CR30","unstructured":"Yaseen N, Yu L, Stanford C, et\u00a0al (2022) Fp4: line-rate greybox fuzz testing for p4 switches. arXiv:2207.13147"}],"container-title":["Journal of King Saud University Computer and Information Sciences"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s44443-025-00083-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s44443-025-00083-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s44443-025-00083-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,7]],"date-time":"2025-07-07T13:03:13Z","timestamp":1751893393000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s44443-025-00083-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6]]},"references-count":30,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2025,6]]}},"alternative-id":["83"],"URL":"https:\/\/doi.org\/10.1007\/s44443-025-00083-6","relation":{},"ISSN":["1319-1578","2213-1248"],"issn-type":[{"value":"1319-1578","type":"print"},{"value":"2213-1248","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,6]]},"assertion":[{"value":"16 March 2025","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"26 May 2025","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"12 June 2025","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"We have no known competing financial interests or personal relationships that could have appeared to influence the work reported in this paper.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing interests"}}],"article-number":"65"}}