{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,11]],"date-time":"2026-07-11T03:28:26Z","timestamp":1783740506508,"version":"3.55.0"},"reference-count":55,"publisher":"IEEE","license":[{"start":{"date-parts":[[2024,10,28]],"date-time":"2024-10-28T00:00:00Z","timestamp":1730073600000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2024,10,28]],"date-time":"2024-10-28T00:00:00Z","timestamp":1730073600000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["CCF-2124116"],"award-info":[{"award-number":["CCF-2124116"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024,10,28]]},"DOI":"10.1109\/icnp61940.2024.10858512","type":"proceedings-article","created":{"date-parts":[[2025,2,4]],"date-time":"2025-02-04T18:29:45Z","timestamp":1738693785000},"page":"1-12","source":"Crossref","is-referenced-by-count":2,"title":["Scalable Verification of Multi-ACK Properties in Loss-Based Congestion Control Implementations"],"prefix":"10.1109","author":[{"given":"Minh","family":"Vu","sequence":"first","affiliation":[{"name":"University of Nebraska-Lincoln"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Hamid","family":"Bagheri","sequence":"additional","affiliation":[{"name":"University of Nebraska-Lincoln"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lisong","family":"Xu","sequence":"additional","affiliation":[{"name":"University of Nebraska-Lincoln"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Wei","family":"Sun","sequence":"additional","affiliation":[{"name":"Meta Platform, Inc"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mingrui","family":"Zhang","sequence":"additional","affiliation":[{"name":"University of Nebraska-Lincoln"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"263","reference":[{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.17487\/rfc5681"},{"key":"ref2","article-title":"CUBIC for fast and long-distance networks","author":"Xu","year":"2023","journal-title":"IETF RFC 9438"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1145\/3009824"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1109\/TNET.2013.2278271"},{"key":"ref5","first-page":"213","article-title":"PacketDrill: Scriptable network stack testing, from sockets to packets","volume-title":"Proceedings of USENIX ATC","author":"Cardwell"},{"key":"ref6","volume-title":"Thanks Google for open source TCP fix","author":"McManus","year":"2015"},{"key":"ref7","first-page":"719","article-title":"Model-agnostic and efficient exploration of numerical state space of real-world TCP congestion control implementations","volume-title":"Proceedings of USENIX Symposium on Networked Systems Design and Implementation (NSDI)","author":"Sun"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1109\/ICC.2018.8422949"},{"key":"ref9","volume-title":"Linux CUBIC Source Code in Latest Kernel"},{"key":"ref10","volume-title":"Linux RENO Source Code in Latest Kernel"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1016\/j.comnet.2006.11.005"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1109\/TNET.2007.896240"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1109\/ICC.2018.8422642"},{"key":"ref14","article-title":"Automated attack discovery in TCP congestion control using a modelguided approach","volume-title":"Proceedings of Network and Distributed Systems Security (NDSS)","author":"Jero"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1145\/3563766.3564088"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1145\/2018436.2018440"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1109\/ICC40277.2020.9149060"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1145\/3452296.3472912"},{"key":"ref19","first-page":"951","article-title":"Towards provably performant congestion control","volume-title":"Proceedings of USENIX Symposium on Networked Systems Design and Implementation (NSDI)","author":"Agarwal"},{"key":"ref20","volume-title":"The Coq proof assistant"},{"key":"ref21","first-page":"221","article-title":"Automated verification of customizable middlebox properties with Gravel","volume-title":"Proceedings of USENIX NSDI","author":"Zhang"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359647"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1145\/3098822.3098833"},{"key":"ref24","article-title":"Model checking large network protocol implementations","volume-title":"Proceedings of USENIX NSDI","author":"Musuvathi"},{"key":"ref25","article-title":"MoDist: Transparent model checking of unmodified distributed systems","volume-title":"Proceedings of USENIX NSDI","author":"Yang"},{"key":"ref26","article-title":"A NICE way to test OpenFlow applications","volume-title":"Proceedings of USENIX NSDI","author":"Canini"},{"key":"ref27","article-title":"NSF workshop on formal methods: Future directions & transition to practice","volume-title":"NSF, Tech. Rep.","author":"Jhala","year":"2012"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1145\/285237.285291"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-56478-9_35"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1016\/0169-7552(89)90019-6"},{"key":"ref31","volume-title":"Network Simulator 3"},{"key":"ref32","article-title":"Pantheon: the training ground for Internet congestion-control research","volume-title":"Proceedings of USENIX ATC","author":"Yan"},{"key":"ref33","article-title":"On inferring TCP behavior","volume-title":"Proceedings of ACM SIGCOMM","author":"Padhye"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1145\/1090191.1080123"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1145\/263109.263160"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-54549-9_9"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1145\/3243650"},{"key":"ref38","first-page":"454","article-title":"Combining model learning and model checking to analyze TCP implementations","volume-title":"Proceedings of Internation Conference on Computer Aided Verification (CAV)","author":"Fiterau-Brosteam"},{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1109\/90.993301"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2015.08.005"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.3923\/jas.2006.1712.1719"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.1145\/3341302.3342087"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132748"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2014.2323977"},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.1109\/INFOCOM.2019.8737390"},{"key":"ref46","first-page":"221","article-title":"Formal methods for network performance analysis","volume-title":"Proceedings of NSDI","author":"Arashloo"},{"key":"ref47","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24622-0_17"},{"key":"ref48","first-page":"130","article-title":"Rule-based static analysis of network protocol implementation","volume-title":"Proceedings of USENIX Security Symposium","author":"Udrea"},{"key":"ref49","doi-asserted-by":"publisher","DOI":"10.1145\/2810103.2813643"},{"key":"ref50","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"ref51","doi-asserted-by":"publisher","DOI":"10.1145\/3182657"},{"key":"ref52","article-title":"KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs","volume-title":"Proceedings of USENIX OSDI","author":"Cadar"},{"key":"ref53","author":"Zhang","journal-title":"[patch net] tcp_cubic fix to achieve at least the same throughput as reno"},{"key":"ref54","volume-title":"Linux Vegas Source Code in Latest Kernel"},{"key":"ref55","doi-asserted-by":"publisher","DOI":"10.1145\/3230543.3230553"}],"event":{"name":"2024 IEEE 32nd International Conference on Network Protocols (ICNP)","location":"Charleroi, Belgium","start":{"date-parts":[[2024,10,28]]},"end":{"date-parts":[[2024,10,31]]}},"container-title":["2024 IEEE 32nd International Conference on Network Protocols (ICNP)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx8\/10858485\/10858498\/10858512.pdf?arnumber=10858512","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,5]],"date-time":"2025-02-05T05:58:29Z","timestamp":1738735109000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/10858512\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,28]]},"references-count":55,"URL":"https:\/\/doi.org\/10.1109\/icnp61940.2024.10858512","relation":{},"subject":[],"published":{"date-parts":[[2024,10,28]]}}}