{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T13:24:53Z","timestamp":1742995493523,"version":"3.40.3"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031660634"},{"type":"electronic","value":"9783031660641"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"DOI":"10.1007\/978-3-031-66064-1_4","type":"book-chapter","created":{"date-parts":[[2024,7,26]],"date-time":"2024-07-26T10:02:00Z","timestamp":1721988120000},"page":"44-63","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Specifying and\u00a0Verifying a\u00a0Real-World Packet Error-Correction System"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9555-8781","authenticated-orcid":false,"given":"Joshua M.","family":"Cohen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6009-0325","authenticated-orcid":false,"given":"Andrew W.","family":"Appel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,7,27]]},"reference":[{"key":"4_CR1","unstructured":"Abhashkumar, A., Gember-Jacobson, A., Akella, A.: Tiramisu: fast multilayer network verification. In: 17th USENIX Symposium on Networked Systems Design and Implementation (NSDI 20), Santa Clara, CA, pp. 201\u2013219. USENIX Association (2020)"},{"key":"4_CR2","doi-asserted-by":"publisher","unstructured":"Alberdingk\u00a0Thijm, T., Beckett, R., Gupta, A., Walker, D.: Modular control plane verification via temporal invariants. Proc. ACM Program. Lang. 7(PLDI) (2023). https:\/\/doi.org\/10.1145\/3591222","DOI":"10.1145\/3591222"},{"key":"4_CR3","doi-asserted-by":"publisher","unstructured":"Appel, A.W.: Verification of a cryptographic primitive: SHA-256. ACM Trans. Program. Lang. Syst. 37(2) (2015). https:\/\/doi.org\/10.1145\/2701415","DOI":"10.1145\/2701415"},{"key":"4_CR4","doi-asserted-by":"publisher","unstructured":"Appel, A.W.: Coq\u2019s vibrant ecosystem for verification engineering (invited talk). In: Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs. CPP 2022, New York, NY, USA, pp. 2\u201311. Association for Computing Machinery (2022). https:\/\/doi.org\/10.1145\/3497775.3503951","DOI":"10.1145\/3497775.3503951"},{"key":"4_CR5","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781107256552","volume-title":"Program Logics for Certified Compilers","author":"AW Appel","year":"2014","unstructured":"Appel, A.W., et al.: Program Logics for Certified Compilers. Cambridge University Press, Cambridge (2014)"},{"key":"4_CR6","doi-asserted-by":"publisher","unstructured":"Arun, V., Arashloo, M.T., Saeed, A., Alizadeh, M., Balakrishnan, H.: Toward formally verifying congestion control behavior. In: Proceedings of the 2021 ACM SIGCOMM 2021 Conference. SIGCOMM \u201921, New York, NY, USA, pp. 1\u201316. Association for Computing Machinery (2021). https:\/\/doi.org\/10.1145\/3452296.3472912","DOI":"10.1145\/3452296.3472912"},{"key":"4_CR7","doi-asserted-by":"publisher","unstructured":"Bare, A.A., Jayasumana, A.P., Banka, T.: Metrics for degree of reordering in packet sequences. In: Proceedings LCN 2002. 27th Annual IEEE Conference on Local Computer Networks, Los Alamitos, CA, USA, p.\u00a00333. IEEE Computer Society (2002). https:\/\/doi.org\/10.1109\/LCN.2002.1181802","DOI":"10.1109\/LCN.2002.1181802"},{"key":"4_CR8","unstructured":"Beckett, R., Gupta, A.: Katra: Realtime verification for multilayer networks. In: 19th USENIX Symposium on Networked Systems Design and Implementation (NSDI 22), pp. 617\u2013634, Renton, WA. USENIX Association (2022)"},{"key":"4_CR9","doi-asserted-by":"publisher","unstructured":"Beckett, R., Gupta, A., Mahajan, R., Walker, D.: A general approach to network configuration verification. In: Proceedings of the Conference of the ACM Special Interest Group on Data Communication. SIGCOMM \u201917, New York, NY, USA, pp. 155\u2013168.. Association for Computing Machinery (2017). https:\/\/doi.org\/10.1145\/3098822.3098834","DOI":"10.1145\/3098822.3098834"},{"key":"4_CR10","doi-asserted-by":"publisher","unstructured":"Bush, R., Elz, R.: Serial Number Arithmetic. RFC 1982 (1996). https:\/\/doi.org\/10.17487\/RFC1982","DOI":"10.17487\/RFC1982"},{"key":"4_CR11","doi-asserted-by":"publisher","unstructured":"Cluzel, G., Georgiou, K., Moy, Y., Zeller, C.: Layered formal verification of a TCP stack. In: 2021 IEEE Secure Development Conference (SecDev), pp. 86\u201393 (2021). https:\/\/doi.org\/10.1109\/SecDev51306.2021.00028","DOI":"10.1109\/SecDev51306.2021.00028"},{"key":"4_CR12","doi-asserted-by":"publisher","unstructured":"Cohen, J.M., Wang, Q., Appel, A.W.: Verified erasure correction in Coq with MathComp and VST. In: Shoham, S., Vizel, Y. (eds.) Computer Aided Verification, pp. 272\u2013292. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-13188-2_14","DOI":"10.1007\/978-3-031-13188-2_14"},{"key":"4_CR13","doi-asserted-by":"publisher","unstructured":"Guo, D., Chen, S., Gao, K., Xiang, Q., Zhang, Y., Yang, Y.R.: Flash: fast, consistent data plane verification for large-scale network settings. In: Proceedings of the ACM SIGCOMM 2022 Conference, pp. 314\u2013335 (2022). https:\/\/doi.org\/10.1145\/3544216.3544246","DOI":"10.1145\/3544216.3544246"},{"key":"4_CR14","doi-asserted-by":"publisher","unstructured":"Hawblitzel, C., et al.: Ironfleet: proving practical distributed systems correct. In: Proceedings of the 25th Symposium on Operating Systems Principles. SOSP \u201915, New York, NY, USA, pp. 1\u201317. Association for Computing Machinery (2015). https:\/\/doi.org\/10.1145\/2815400.2815428","DOI":"10.1145\/2815400.2815428"},{"key":"4_CR15","doi-asserted-by":"publisher","unstructured":"Kellison, A.E., Appel, A.W.: Verified numerical methods for ordinary differential equations. In: Isac, O., Ivanov, R., Katz, G., Narodytska, N., Nenzi, L. (eds.) Software Verification and Formal Methods for ML-Enabled Autonomous Systems, pp. 147\u2013163. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-21222-2_9","DOI":"10.1007\/978-3-031-21222-2_9"},{"issue":"7","key":"4_CR16","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009). https:\/\/doi.org\/10.1145\/1538788.1538814","journal-title":"Commun. ACM"},{"key":"4_CR17","doi-asserted-by":"publisher","unstructured":"McAuley, A.J.: Reliable broadband communication using a burst erasure correcting code. In: Proceedings of the ACM Symposium on Communications Architectures & Protocols. SIGCOMM \u201990, New York, NY, USA, pp. 297\u2013306 (1990). https:\/\/doi.org\/10.1145\/99508.99566","DOI":"10.1145\/99508.99566"},{"key":"4_CR18","doi-asserted-by":"publisher","unstructured":"Morton, A., Ramachandran, G., Shalunov, S., Ciavattone, L., Perser, J.: Packet Reordering Metrics. RFC 4737 (2006). https:\/\/doi.org\/10.17487\/RFC4737","DOI":"10.17487\/RFC4737"},{"issue":"1","key":"4_CR19","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1002\/dac.884","volume":"21","author":"NM Piratla","year":"2008","unstructured":"Piratla, N.M., Jayasumana, A.P.: Metrics for packet reordering-a comparative analysis. Int. J. Commun. Syst. 21(1), 99\u2013113 (2008). https:\/\/doi.org\/10.1002\/dac.884","journal-title":"Int. J. Commun. Syst."},{"key":"4_CR20","doi-asserted-by":"publisher","unstructured":"Piratla, N.M., Jayasumana, A.P., Bare, A.A.: Reorder density (RD): a formal, comprehensive metric for packet reordering. In: Boutaba, R., Almeroth, K., Puigjaner, R., Shen, S., Black, J.P. (eds.) NETWORKING 2005. Networking Technologies, Services, and Protocols; Performance of Computer and Communication Networks; Mobile and Wireless Communications Systems. pp. 78\u201389. Springer, Cham (2005). https:\/\/doi.org\/10.1007\/11422778_7","DOI":"10.1007\/11422778_7"},{"key":"4_CR21","unstructured":"Pirelli, S., Valentukonyt\u0117, A., Argyraki, K., Candea, G.: Automated verification of network function binaries. In: 19th USENIX Symposium on Networked Systems Design and Implementation (NSDI 22), Renton, WA, pp. 585\u2013600. USENIX Association (2022)"},{"issue":"2","key":"4_CR22","doi-asserted-by":"publisher","first-page":"300","DOI":"10.1137\/0108018","volume":"8","author":"IS Reed","year":"1960","unstructured":"Reed, I.S., Solomon, G.: Polynomial codes over certain finite fields. J. Soc. Ind. Appl. Math. 8(2), 300\u2013304 (1960). https:\/\/doi.org\/10.1137\/0108018","journal-title":"J. Soc. Ind. Appl. Math."},{"key":"4_CR23","doi-asserted-by":"publisher","unstructured":"Uijterwaal, D.H.A.: A One-Way Packet Duplication Metric. RFC 5560 (2009). https:\/\/doi.org\/10.17487\/RFC5560","DOI":"10.17487\/RFC5560"},{"key":"4_CR24","doi-asserted-by":"publisher","unstructured":"Whitner, R., Banka, T., Piratla, N.M., Bare, A.A., Jayasumana, P.A.P.: Improved Packet Reordering Metrics. RFC 5236 (2008). https:\/\/doi.org\/10.17487\/RFC5236","DOI":"10.17487\/RFC5236"},{"key":"4_CR25","doi-asserted-by":"publisher","unstructured":"Wilcox, J.R., et al.: Verdi: a framework for implementing and formally verifying distributed systems. In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation. PLDI \u201915, New York, NY, USA, pp. 357\u2013368. Association for Computing Machinery (2015). https:\/\/doi.org\/10.1145\/2737924.2737958","DOI":"10.1145\/2737924.2737958"},{"key":"4_CR26","doi-asserted-by":"publisher","unstructured":"Ye, F., et al.: Accuracy, scalability, coverage: a practical configuration verifier on a global wan. 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. SIGCOMM \u201920, New York, NY, USA, pp. 599\u2013614. Association for Computing Machinery (2020). https:\/\/doi.org\/10.1145\/3387514.3406217","DOI":"10.1145\/3387514.3406217"},{"key":"4_CR27","doi-asserted-by":"publisher","unstructured":"Ye, K.Q., Green, M., Sanguansin, N., Beringer, L., Petcher, A., Appel, A.W.: Verified correctness and security of MbedTLS HMAC-DRBG. In: Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security. CCS \u201917, New York, NY, USA, pp. 2007\u20132020 (2017). https:\/\/doi.org\/10.1145\/3133956.3133974","DOI":"10.1145\/3133956.3133974"},{"key":"4_CR28","doi-asserted-by":"publisher","unstructured":"Zaostrovnykh, A., et al.: Verifying software network functions with no verification expertise. In: Proceedings of the 27th ACM Symposium on Operating Systems Principles. SOSP \u201919, New York, NY, USA, pp. 275\u2013290 (2019). https:\/\/doi.org\/10.1145\/3341301.3359647","DOI":"10.1145\/3341301.3359647"},{"key":"4_CR29","doi-asserted-by":"publisher","unstructured":"Zaostrovnykh, A., Pirelli, S., Pedrosa, L., Argyraki, K., Candea, G.: A formally verified NAT. In: Proceedings of the Conference of the ACM Special Interest Group on Data Communication. SIGCOMM \u201917, New York, NY, USA, pp. 141\u2013154 (2017). doi: https:\/\/doi.org\/10.1145\/3098822.3098833","DOI":"10.1145\/3098822.3098833"},{"key":"4_CR30","doi-asserted-by":"publisher","unstructured":"Zhang, H., et al.: Verifying an HTTP key-value server with interaction trees and VST. In: Cohen, L., Kaliszyk, C. (eds.) 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0193, pp. 32:1\u201332:19. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2021). https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2021.32","DOI":"10.4230\/LIPIcs.ITP.2021.32"},{"key":"4_CR31","unstructured":"Zhang, K., Zhuo, D., Akella, A., Krishnamurthy, A., Wang, X.: Automated verification of customizable middlebox properties with Gravel. In: 17th USENIX Symposium on Networked Systems Design and Implementation (NSDI 20), Santa Clara, CA, pp. 221\u2013239. USENIX Association (2020)"},{"key":"4_CR32","doi-asserted-by":"publisher","unstructured":"Zhang, P., Wang, D., Gember-Jacobson, A.: Symbolic router execution. In: Proceedings of the ACM SIGCOMM 2022 Conference. SIGCOMM \u201922, New York, NY, USA, pp. 336\u2013349. Association for Computing Machinery (2022). https:\/\/doi.org\/10.1145\/3544216.3544264","DOI":"10.1145\/3544216.3544264"}],"container-title":["Lecture Notes in Computer Science","Verified Software. Theories, Tools and Experiments"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-66064-1_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,26]],"date-time":"2024-07-26T10:02:19Z","timestamp":1721988139000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-66064-1_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031660634","9783031660641"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-66064-1_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"27 July 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"VSTTE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Verified Software: Theories, Tools, and Experiments","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Ames, IA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 October 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 October 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vstte2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/homepage.cs.uiowa.edu\/~ajreynol\/VSTTE2023\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}