{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T10:52:27Z","timestamp":1770288747694,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":41,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,6,8]],"date-time":"2019-06-08T00:00:00Z","timestamp":1559952000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100011199","name":"European Research Council","doi-asserted-by":"publisher","award":["679127"],"award-info":[{"award-number":["679127"]}],"id":[{"id":"10.13039\/100011199","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["NeTS-1413972 and AiTF-1637532"],"award-info":[{"award-number":["NeTS-1413972 and AiTF-1637532"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2019,6,8]]},"DOI":"10.1145\/3314221.3314639","type":"proceedings-article","created":{"date-parts":[[2019,6,7]],"date-time":"2019-06-07T21:02:18Z","timestamp":1559941338000},"page":"190-203","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":22,"title":["Scalable verification of probabilistic networks"],"prefix":"10.1145","author":[{"given":"Steffen","family":"Smolka","sequence":"first","affiliation":[{"name":"Cornell University, USA"}]},{"given":"Praveen","family":"Kumar","sequence":"additional","affiliation":[{"name":"Cornell University, USA"}]},{"given":"David M.","family":"Kahn","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, USA"}]},{"given":"Nate","family":"Foster","sequence":"additional","affiliation":[{"name":"Cornell University, USA"}]},{"given":"Justin","family":"Hsu","sequence":"additional","affiliation":[{"name":"University of Wisconsin-Madison, USA"}]},{"given":"Dexter","family":"Kozen","sequence":"additional","affiliation":[{"name":"Cornell University, USA"}]},{"given":"Alexandra","family":"Silva","sequence":"additional","affiliation":[{"name":"University College London, UK"}]}],"member":"320","published-online":{"date-parts":[[2019,6,8]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1978.1675141"},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1402946.1402967"},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535862"},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"crossref","unstructured":"Manav Bhatia Mach Chen Sami Boutros Marc Binderberger and Jeffrey Haas. 2014. Bidirectional Forwarding Detection (BFD) on Link Aggregation Group (LAG) Interfaces. RFC 7130.  Manav Bhatia Mach Chen Sami Boutros Marc Binderberger and Jeffrey Haas. 2014. Bidirectional Forwarding Detection (BFD) on Link Aggregation Group (LAG) Interfaces. RFC 7130.","DOI":"10.17487\/rfc7130"},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2656877.2656890"},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2661061.2661063"},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/992200.992206"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exi008"},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/1251375.1251396"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"crossref","unstructured":"A. Dixit P. Prakash Y. C. Hu and R. R. Kompella. 2013. On the impact of packet spraying in data center networks. In IEEE INFOCOM. 2130\u2013 2138.  A. Dixit P. Prakash Y. C. Hu and R. R. Kompella. 2013. On the impact of packet spraying in data center networks. In IEEE INFOCOM. 2130\u2013 2138.","DOI":"10.1109\/INFCOM.2013.6567015"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"crossref","unstructured":"Nate Foster Dexter Kozen Konstantinos Mamouras Mark Reitblatt and Alexandra Silva. 2016. Probabilistic NetKAT. In ESOP. 282\u2013309.  Nate Foster Dexter Kozen Konstantinos Mamouras Mark Reitblatt and Alexandra Silva. 2016. Probabilistic NetKAT. In ESOP. 282\u2013309.","DOI":"10.1007\/978-3-662-49498-1_12"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677011"},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008647823331"},{"key":"e_1_3_2_2_14_1","volume-title":"Vechev","author":"Gehr Timon","year":"2018","unstructured":"Timon Gehr , Sasa Misailovic , Petar Tsankov , Laurent Vanbever , Pascal Wiesmann , and Martin T . Vechev . 2018 . Bayonet : Probabilistic Computer Network Analysis . Available at https:\/\/github.com\/eth-sri\/ bayonet\/ . Timon Gehr, Sasa Misailovic, Petar Tsankov, Laurent Vanbever, Pascal Wiesmann, and Martin T. Vechev. 2018. Bayonet: Probabilistic Computer Network Analysis. Available at https:\/\/github.com\/eth-sri\/ bayonet\/ ."},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192400"},{"key":"e_1_3_2_2_16_1","volume-title":"Vechev","author":"Gehr Timon","year":"2016","unstructured":"Timon Gehr , Sasa Misailovic , and Martin T . Vechev . 2016 . PSI : Exact Symbolic Inference for Probabilistic Programs . 62\u201383. Timon Gehr, Sasa Misailovic, and Martin T. Vechev. 2016. PSI: Exact Symbolic Inference for Probabilistic Programs. 62\u201383."},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2018436.2018477"},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2593882.2593900"},{"key":"e_1_3_2_2_19_1","first-page":"113","article-title":"Header Space Analysis","volume":"2012","author":"Kazemian Peyman","year":"2012","unstructured":"Peyman Kazemian , George Varghese , and Nick McKeown . 2012 . Header Space Analysis : Static Checking for Networks. In USENIX NSDI 2012. 113 \u2013 126 . https:\/\/www.usenix.org\/conference\/nsdi12\/ technical-sessions\/presentation\/kazemian Peyman Kazemian, George Varghese, and Nick McKeown. 2012. Header Space Analysis: Static Checking for Networks. In USENIX NSDI 2012. 113\u2013126. https:\/\/www.usenix.org\/conference\/nsdi12\/ technical-sessions\/presentation\/kazemian","journal-title":"Static Checking for Networks. In USENIX NSDI"},{"key":"e_1_3_2_2_20_1","volume-title":"Finite markov chains","author":"Kemeny John G","unstructured":"John G Kemeny and James Laurie Snell . 1960. Finite markov chains . Vol. 356 . van Nostrand Princeton , NJ. John G Kemeny and James Laurie Snell. 1960. Finite markov chains. Vol. 356. van Nostrand Princeton, NJ."},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2377677.2377766"},{"key":"e_1_3_2_2_22_1","volume-title":"Chiun Lin Lim, and Robert Soul\u00e9","author":"Kumar Praveen","year":"2018","unstructured":"Praveen Kumar , Yang Yuan , Chris Yu , Nate Foster , Robert Kleinberg , Petr Lapukhov , Chiun Lin Lim, and Robert Soul\u00e9 . 2018 . Semi-Oblivious Traffic Engineering: The Road Not Taken. In USENIX NSDI. Praveen Kumar, Yang Yuan, Chris Yu, Nate Foster, Robert Kleinberg, Petr Lapukhov, Chiun Lin Lim, and Robert Soul\u00e9. 2018. Semi-Oblivious Traffic Engineering: The Road Not Taken. In USENIX NSDI."},{"key":"e_1_3_2_2_23_1","volume-title":"Proc. 23rd International Conference on Computer Aided Verification (CAV\u201911)","volume":"6806","author":"Kwiatkowska M.","unstructured":"M. Kwiatkowska , G. Norman , and D. Parker . 2011. PRISM 4.0: Verification of Probabilistic Real-time Systems . In Proc. 23rd International Conference on Computer Aided Verification (CAV\u201911) (LNCS), G. Gopalakrishnan and S. Qadeer (Eds.) , Vol. 6806 . Springer, 585\u2013591. M. Kwiatkowska, G. Norman, and D. Parker. 2011. PRISM 4.0: Verification of Probabilistic Real-time Systems. In Proc. 23rd International Conference on Computer Aided Verification (CAV\u201911) (LNCS), G. Gopalakrishnan and S. Qadeer (Eds.), Vol. 6806. Springer, 585\u2013591."},{"key":"e_1_3_2_2_24_1","doi-asserted-by":"crossref","unstructured":"Marta Z. Kwiatkowska Gethin Norman and David Parker. 2011. PRISM 4.0: Verification of Probabilistic Real-Time Systems. In CAV. 585\u2013591.   Marta Z. Kwiatkowska Gethin Norman and David Parker. 2011. PRISM 4.0: Verification of Probabilistic Real-Time Systems. In CAV. 585\u2013591.","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"crossref","unstructured":"Jed Liu William Hallahan Cole Schlesinger Milad Sharif Jeongkeun Lee Robert Soul\u00e9 Han Wang Calin Cascaval Nick McKeown and Nate Foster. 2018. p4v: Practical Verification for Programmable Data Planes. In SIGCOMM. 490\u2013503.  Jed Liu William Hallahan Cole Schlesinger Milad Sharif Jeongkeun Lee Robert Soul\u00e9 Han Wang Calin Cascaval Nick McKeown and Nate Foster. 2018. p4v: Practical Verification for Programmable Data Planes. In SIGCOMM. 490\u2013503.","DOI":"10.1145\/3230543.3230582"},{"key":"e_1_3_2_2_26_1","unstructured":"Vincent Liu Daniel Halperin Arvind Krishnamurthy and Thomas E Anderson. 2013. F10: A Fault-Tolerant Engineered Network. In USENIX NSDI. 399\u2013412.   Vincent Liu Daniel Halperin Arvind Krishnamurthy and Thomas E Anderson. 2013. F10: A Fault-Tolerant Engineered Network. In USENIX NSDI. 399\u2013412."},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2018436.2018470"},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1355734.1355746"},{"key":"e_1_3_2_2_29_1","unstructured":"Maciej Olejnik Herbert Wiklicky and Mahdi Cheraghchi. 2016. Probabilistic Programming and Discrete Time Markov Chains. http:\/\/www.imperial.ac.uk\/media\/imperial-college\/ faculty-of-engineering\/computing\/public\/MaciejOlejnik.pdf  Maciej Olejnik Herbert Wiklicky and Mahdi Cheraghchi. 2016. Probabilistic Programming and Discrete Time Markov Chains. http:\/\/www.imperial.ac.uk\/media\/imperial-college\/ faculty-of-engineering\/computing\/public\/MaciejOlejnik.pdf"},{"key":"e_1_3_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2785956.2787472"},{"key":"e_1_3_2_2_31_1","volume-title":"Ramana Rao Kompella, and David G. Andersen","author":"Sekar Vyas","year":"2008","unstructured":"Vyas Sekar , Michael K. Reiter , Walter Willinger , Hui Zhang , Ramana Rao Kompella, and David G. Andersen . 2008 . CSAMP : A System for Network-wide Flow Monitoring. In USENIX NSDI. 233\u2013246. Vyas Sekar, Michael K. Reiter, Walter Willinger, Hui Zhang, Ramana Rao Kompella, and David G. Andersen. 2008. CSAMP: A System for Network-wide Flow Monitoring. In USENIX NSDI. 233\u2013246."},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1137\/0213021"},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3230543.3230570"},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784761"},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009843"},{"key":"e_1_3_2_2_36_1","volume-title":"Scalable Verification of Probabilistic Networks (Extended Version). arXiv","author":"Smolka Steffen","year":"2019","unstructured":"Steffen Smolka , Praveen Kumar , David M Kahn , Nate Foster , Justin Hsu , Dexter Kozen , and Alexandra Silva . 2019. Scalable Verification of Probabilistic Networks (Extended Version). arXiv ( 2019 ). arXiv: 1904.08096 Steffen Smolka, Praveen Kumar, David M Kahn, Nate Foster, Justin Hsu, Dexter Kozen, and Alexandra Silva. 2019. Scalable Verification of Probabilistic Networks (Extended Version). arXiv (2019). arXiv: 1904.08096"},{"key":"e_1_3_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/363347.363387"},{"key":"e_1_3_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1137\/0211027"},{"key":"e_1_3_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3211994"},{"key":"e_1_3_2_2_40_1","unstructured":"Geoffrey G. Xie Jibin Zhan David A. Maltz Hui Zhang Albert G. Greenberg G\u00edsli Hj\u00e1lmt\u00fdsson and Jennifer Rexford. 2005. On static reachability analysis of IP networks. In INFOCOM.  Geoffrey G. Xie Jibin Zhan David A. Maltz Hui Zhang Albert G. Greenberg G\u00edsli Hj\u00e1lmt\u00fdsson and Jennifer Rexford. 2005. On static reachability analysis of IP networks. In INFOCOM."},{"key":"e_1_3_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2619239.2626308"}],"event":{"name":"PLDI '19: 40th ACM SIGPLAN Conference on Programming Language Design and Implementation","location":"Phoenix AZ USA","acronym":"PLDI '19","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3314221.3314639","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3314221.3314639","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3314221.3314639","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:53:22Z","timestamp":1750204402000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3314221.3314639"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,6,8]]},"references-count":41,"alternative-id":["10.1145\/3314221.3314639","10.1145\/3314221"],"URL":"https:\/\/doi.org\/10.1145\/3314221.3314639","relation":{},"subject":[],"published":{"date-parts":[[2019,6,8]]},"assertion":[{"value":"2019-06-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}