{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:13:05Z","timestamp":1750306385004,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":53,"publisher":"ACM","license":[{"start":{"date-parts":[[2015,7,14]],"date-time":"2015-07-14T00:00:00Z","timestamp":1436832000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CNS-1218066,CNS-1117052,CNS-0845552"],"award-info":[{"award-number":["CNS-1218066,CNS-1117052,CNS-0845552"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000181","name":"Air Force Office of Scientific Research","doi-asserted-by":"publisher","award":["Young Investigator Award FA9550-12-1-0327"],"award-info":[{"award-number":["Young Investigator Award FA9550-12-1-0327"]}],"id":[{"id":"10.13039\/100000181","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2015,7,14]]},"DOI":"10.1145\/2790449.2790516","type":"proceedings-article","created":{"date-parts":[[2015,6,29]],"date-time":"2015-06-29T18:10:47Z","timestamp":1435601447000},"page":"79-90","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Automated verification of safety properties of declarative networking programs"],"prefix":"10.1145","author":[{"given":"Chen","family":"Chen","sequence":"first","affiliation":[{"name":"University Of Pennsylvania"}]},{"given":"Lay Kuan","family":"Loh","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University"}]},{"given":"Limin","family":"Jia","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University"}]},{"given":"Wenchao","family":"Zhou","sequence":"additional","affiliation":[{"name":"Georgetown University"}]},{"given":"Boon Thau","family":"Loo","sequence":"additional","affiliation":[{"name":"University Of Pennsylvania"}]}],"member":"320","published-online":{"date-parts":[[2015,7,14]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1866898.1866905"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/INFCOM.2004.1354680"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1755913.1755937"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2010.12"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/2032266.2032272"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/IROS.2007.4399480"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594317"},{"key":"e_1_3_2_1_9_1","volume-title":"NSDI","author":"Canini M.","year":"2012","unstructured":"M. Canini , D. Venzano , P. Peresini , D. Kostic , and J. Rexford . A nice way to test openflow applications . In NSDI , 2012 . M. Canini, D. Venzano, P. Peresini, D. Kostic, and J. Rexford. A nice way to test openflow applications. In NSDI, 2012."},{"key":"e_1_3_2_1_10_1","volume-title":"FORTE","author":"Chen C.","year":"2014","unstructured":"C. Chen , L. Jia , H. Xu , C. Luo , W. Zhou , and B. T. Loo . A program logic for verifying secure routing protocols . In FORTE , 2014 . C. Chen, L. Jia, H. Xu, C. Luo, W. Zhou, and B. T. Loo. A program logic for verifying secure routing protocols. In FORTE, 2014."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1921168.1921176"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1322263.1322281"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28641-4_3"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068414000167"},{"key":"e_1_3_2_1_16_1","volume-title":"NSDI","author":"Engler D.","year":"2004","unstructured":"D. Engler and M. Musuvathi . Model-checking large network protocol implementations . In NSDI , 2004 . D. Engler and M. Musuvathi. Model-checking large network protocol implementations. In NSDI, 2004."},{"key":"e_1_3_2_1_17_1","volume-title":"NDSI","author":"Feamster N.","year":"2005","unstructured":"N. Feamster and H. Balakrishnan . Detecting bgp configuration faults with static analysis . In NDSI , 2005 . N. Feamster and H. Balakrishnan. Detecting bgp configuration faults with static analysis. In NDSI, 2005."},{"key":"e_1_3_2_1_18_1","volume-title":"NSDI","author":"Fogel A.","year":"2015","unstructured":"A. Fogel , S. Fung , L. Pedrosa , M. Walraed-Sullivan , R. Govindan , R. Mahajan , and T. Millstein . A general approach to network configuration analysis . In NSDI , 2015 . A. Fogel, S. Fung, L. Pedrosa, M. Walraed-Sullivan, R. Govindan, R. Mahajan, and T. Millstein. A general approach to network configuration analysis. In NSDI, 2015."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1045405.1045413"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11503-5_9"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2342441.2342458"},{"key":"e_1_3_2_1_22_1","volume-title":"NSDI","author":"Kazemian P.","year":"2012","unstructured":"P. Kazemian , G. Varghese , and N. McKeown . Header space analysis: static checking for networks . In NSDI , 2012 . P. Kazemian, G. Varghese, and N. McKeown. Header space analysis: static checking for networks. In NSDI, 2012."},{"key":"e_1_3_2_1_23_1","volume-title":"NSDI","author":"Kazemian P.","year":"2013","unstructured":"P. Kazemian , M. Chan , H. Zeng , G. Varghese , N. McKeown , and S. Whyte . Real time network policy checking using header space analysis . In NSDI , 2013 . P. Kazemian, M. Chan, H. Zeng, G. Varghese, N. McKeown, and S. Whyte. Real time network policy checking using header space analysis. In NSDI, 2013."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2342441.2342452"},{"key":"e_1_3_2_1_25_1","volume-title":"NSDI","author":"Killian C.","year":"2007","unstructured":"C. Killian , J. Anderson , R. Jhala , and A. Vahdat . Life, death, and the critical transition: Finding liveness bugs in systems code . In NSDI , 2007 . C. Killian, J. Anderson, R. Jhala, and A. Vahdat. Life, death, and the critical transition: Finding liveness bugs in systems code. In NSDI, 2007."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/COMSNETS.2012.6151315"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/TNET.2011.2165851"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1095810.1095818"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1080091.1080126"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1142473.1142485"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1592761.1592785"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068410000360"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2018436.2018470"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1544012.1544017"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1355734.1355746"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1614293.1614295"},{"key":"e_1_3_2_1_37_1","volume-title":"LISA","author":"Nelson T.","year":"2010","unstructured":"T. Nelson , C. Barratt , D. Dougherty , K. Fisler , and S. Krishnamurthi . The margrave tool for firewall analysis . In LISA , 2010 . T. Nelson, C. Barratt, D. Dougherty, K. Fisler, and S. Krishnamurthi. The margrave tool for firewall analysis. In LISA, 2010."},{"key":"e_1_3_2_1_38_1","volume-title":"NSDI","author":"Nelson T.","year":"2014","unstructured":"T. Nelson , A. D. Ferguson , M. J. G. Scheer , and S. Krishnamurthi . Tierless programming and reasoning for software-defined networks . In NSDI , 2014 . T. Nelson, A. D. Ferguson, M. J. G. Scheer, and S. Krishnamurthi. Tierless programming and reasoning for software-defined networks. In NSDI, 2014."},{"key":"e_1_3_2_1_39_1","unstructured":"Network Simulator 3. http:\/\/www.nsnam.org\/.  Network Simulator 3. http:\/\/www.nsnam.org\/."},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2003476.2003495"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2342441.2342466"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(94)00039-9"},{"key":"e_1_3_2_1_43_1","unstructured":"RapidNet. http:\/\/netdb.cis.upenn.edu\/rapidnet\/.  RapidNet. http:\/\/netdb.cis.upenn.edu\/rapidnet\/."},{"key":"e_1_3_2_1_44_1","volume-title":"NDSS","author":"Sherr M.","year":"2010","unstructured":"M. Sherr , A. Mao , W. R. Marczak , W. Zhou , B. T. Loo , and M. Blaze . A3: An extensible platform for application-aware anonymity . In NDSS , 2010 . M. Sherr, A. Mao, W. R. Marczak, W. Zhou, B. T. Loo, and M. Blaze. A3: An extensible platform for application-aware anonymity. In NDSS, 2010."},{"key":"e_1_3_2_1_45_1","volume-title":"NSDI","author":"Singh A.","year":"2008","unstructured":"A. Singh , T. Das , P. Maniatis , P. Druschel , and T. Roscoe . BFT Protocols Under Fire . In NSDI , 2008 . A. Singh, T. Das, P. Maniatis, P. Druschel, and T. Roscoe. BFT Protocols Under Fire. In NSDI, 2008."},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2461446.2461461"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-92995-6_5"},{"key":"e_1_3_2_1_48_1","volume-title":"TPHOLs","author":"Wang A.","year":"2009","unstructured":"A. Wang , B. T. Loo , C. Liu , O. Sokolsky , and P. Basu . A Theorem Proving Approach towards Declarative Networking . In TPHOLs , 2009 . A. Wang, B. T. Loo, C. Liu, O. Sokolsky, and P. Basu. A Theorem Proving Approach towards Declarative Networking. In TPHOLs, 2009."},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2006.16"},{"key":"e_1_3_2_1_50_1","unstructured":"Z3. http:\/\/z3.codeplex.com\/.  Z3. http:\/\/z3.codeplex.com\/."},{"key":"e_1_3_2_1_51_1","volume-title":"NSDI","author":"Zeng H.","year":"2014","unstructured":"H. Zeng , S. Zhang , F. Ye , V. Jeyakumar , M. Ju , J. Liu , N. McKeown , and A. Vahdat . Libra: Divide and conquer to verify forwarding tables in huge networks . In NSDI , 2014 . H. Zeng, S. Zhang, F. Ye, V. Jeyakumar, M. Ju, J. Liu, N. McKeown, and A. Vahdat. Libra: Divide and conquer to verify forwarding tables in huge networks. In NSDI, 2014."},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660267.2660349"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/1807167.1807234"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/2043556.2043584"},{"key":"e_1_3_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.14778\/2535568.2448939"}],"event":{"name":"PPDP '15: 17th International Symposium on Principles and Practice of Declarative Programming","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"],"location":"Siena Italy","acronym":"PPDP '15"},"container-title":["Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2790449.2790516","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2790449.2790516","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T05:07:06Z","timestamp":1750223226000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2790449.2790516"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,7,14]]},"references-count":53,"alternative-id":["10.1145\/2790449.2790516","10.1145\/2790449"],"URL":"https:\/\/doi.org\/10.1145\/2790449.2790516","relation":{},"subject":[],"published":{"date-parts":[[2015,7,14]]},"assertion":[{"value":"2015-07-14","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}