{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,29]],"date-time":"2024-10-29T13:33:08Z","timestamp":1730208788843,"version":"3.28.0"},"reference-count":31,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015,11]]},"DOI":"10.1109\/cnsm.2015.7367384","type":"proceedings-article","created":{"date-parts":[[2016,1,4]],"date-time":"2016-01-04T16:34:58Z","timestamp":1451925298000},"page":"366-371","source":"Crossref","is-referenced-by-count":4,"title":["Demonstrating topoS: Theorem-prover-based synthesis of secure network configurations"],"prefix":"10.1109","author":[{"given":"Cornelius","family":"Diekmann","sequence":"first","affiliation":[]},{"given":"Andreas","family":"Korsten","sequence":"additional","affiliation":[]},{"given":"Georg","family":"Carle","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1109\/INM.2015.7140326"},{"key":"ref30","first-page":"1","article-title":"Policy refinement: Decomposition and operationalization for dynamic domains","author":"craven","year":"2011","journal-title":"CNSM"},{"key":"ref10","volume":"2283","author":"nipkow","year":"2002","journal-title":"Isabelle\/HOL A Proof Assistant for Higher-Order Logic"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1109\/SURV.2012.090512.00043"},{"key":"ref12","first-page":"1","article-title":"Composing software defined networks","author":"monsanto","year":"2013","journal-title":"NSDI USENIX"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784761"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1109\/INFCOM.2005.1498492"},{"article-title":"Network verification in the light of program verification","year":"2013","author":"lopes","key":"ref15"},{"key":"ref16","article-title":"Header space analysis: static checking for networks","author":"kazemian","year":"2012","journal-title":"NSDI USENIX"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1145\/2043164.2018470"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1109\/ICNP.2009.5339690"},{"key":"ref19","first-page":"15","article-title":"Veriflow: Verifying network-wide invariants in real time","author":"khurshid","year":"2013","journal-title":"NSDI USENIX"},{"key":"ref28","first-page":"43","article-title":"Detecting BGP configuration faults with static analysis","author":"feamster","year":"2005","journal-title":"NSDI"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2004.2"},{"key":"ref27","article-title":"Semantics-preserving simplification of real-world firewall rule sets","author":"diekmann","year":"2015","journal-title":"Formal Methods"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1145\/1266840.1266871"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1145\/2342356.2342359"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33386-6_1"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1109\/MCOM.2006.1607877"},{"key":"ref8","article-title":"Network security policy verification","author":"diekmann","year":"2014","journal-title":"Archive of Formal Proofs"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-43613-4_9"},{"key":"ref2","first-page":"199","article-title":"FIREMAN: a toolkit for firewall modeling and analysis","author":"yuan","year":"2006","journal-title":"IEEE S&P"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.150.3"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1145\/2379690.2379691"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1109\/SECPRI.1999.766714"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1145\/2674005.2674989"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1145\/2342441.2342466"},{"key":"ref24","first-page":"15","article-title":"Design and implementation of a routing control platform","author":"caesar","year":"2005","journal-title":"NSDI"},{"key":"ref23","first-page":"59","article-title":"Kinetic: Verifiable dynamic network control","author":"kim","year":"2015","journal-title":"NSDI"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1145\/2535372.2535373"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1145\/1355734.1355746"}],"event":{"name":"2015 11th International Conference on Network and Service Management (CNSM)","start":{"date-parts":[[2015,11,9]]},"location":"Barcelona, Spain","end":{"date-parts":[[2015,11,13]]}},"container-title":["2015 11th International Conference on Network and Service Management (CNSM)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/7360263\/7367318\/07367384.pdf?arnumber=7367384","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,3,24]],"date-time":"2017-03-24T21:24:43Z","timestamp":1490390683000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/7367384\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,11]]},"references-count":31,"URL":"https:\/\/doi.org\/10.1109\/cnsm.2015.7367384","relation":{},"subject":[],"published":{"date-parts":[[2015,11]]}}}