Quelle  root.bib

@inproceedings{nelson2015exodus,
 title={Exodus: toward automatic migration of enterprise network configurations to {SDN}s},
 author={Nelson, Tim and Ferguson, Andrew D and Yu, Da and Fonseca, Rodrigo and Krishnamurthi, Shriram},
 booktitle={Proceedings of the 1st ACM SIGCOMM Symposium on Software Defined Networking Research},
 pages={13},
 year={2015},
 organization={ACM}
}

@inproceedings{guha2013machine,
 author = {Guha, Arjun and Reitblatt, Mark and Foster, Nate},
 title = {{M}achine-verified {N}etwork {C}ontrollers},
 booktitle = {Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation},
 series = {PLDI '13},
 year = {2013},
 isbn = {978-1-4503-2014-6},
 location = {Seattle, Washington, USA},
 pages = {483--494},
 numpages = {12},
 url = {http://doi.acm.org/10.1145/2491956.2462178},
 doi = {10.1145/2491956.2462178},
 acmid = {2462178},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {coq, domain-specific languages, formal verification, frenetic, netcore, openflow, software-defined networking},
}
@inproceedings{dobrescu2014software,
 title={Software dataplane verification},
 author={Dobrescu, Mihai and Argyraki, Katerina},
 booktitle={Proceedings of the 11th Symposium on Networked Systems Design and Implementation (NSDI), Seattle, WA},
 year={2014}
}
@inproceedings{zhang2000intrusion,
 title={Intrusion detection in wireless ad-hoc networks},
 author={Zhang, Yongguang and Lee, Wenke},
 booktitle={Proceedings of the 6th annual international conference on Mobile computing and networking},
 pages={275--283},
 year={2000},
 organization={ACM}
}
@inproceedings{nelson2010margrave,
 title={{The Margrave Tool for Firewall Analysis}},
 author={Nelson, Timothy and Barratt, Christopher and Dougherty, Daniel J and Fisler, Kathi and Krishnamurthi, Shriram},
 booktitle={Proceedings of the Large Installation System Administration Conference},
 year={2010}
}
@inproceedings {kazemian12header,
 author = {Peyman Kazemian and George Varghese and Nick McKeown},
 title = {{Header Space Analysis: Static Checking for Networks}},
 booktitle = {Presented as part of the 9th USENIX Symposium on Networked Systems Design and Implementation (NSDI 12)},
 year = {2012},
 isbn = {978-931971-92-8},
 address = {San Jose, CA},
 pages = {113--126},
 url = {https://www.usenix.org/conference/nsdi12/technical-sessions/presentation/kazemian},
 publisher = {USENIX},
}
@inproceedings{ball2014vericon,
 title={Veri{C}on: {T}owards verifying controller programs in software-defined networks},
 author={Ball, Thomas and Bj{\o}rner, Nikolaj and Gember, Aaron and Itzhaky, Shachar and Karbyshev, Aleksandr and Sagiv, Mooly and Schapira, Michael and Valadarsky, Asaf},
 booktitle={ACM SIGPLAN Notices},
 volume={49},
 pages={282--293},
 year={2014},
 organization={ACM}
}
@incollection{brucker2007test,
 title={Test-{S}equence {G}eneration with {HOL}-{T}est{G}en with an {A}pplication to {F}irewall {T}esting},
 author={Brucker, Achim D and Wolff, Burkhart},
 booktitle={Tests and Proofs},
 pages={149--168},
 year={2007},
 publisher={Springer}
}
@incollection{brucker2008model,
 title={Model-based firewall conformance testing},
 author={Brucker, Achim D and Br{\"u}gger, Lukas and Wolff, Burkhart},
 booktitle={Testing of Software and Communicating Systems},
 pages={103--118},
 year={2008},
 publisher={Springer}
}
@inproceedings{brucker2010verified,
 title={Verified firewall policy transformations for test case generation},
 author={Brucker, Achim D and Brügger, Lukas and Kearney, Paul and Wolff, Burkhart},
 booktitle={Software Testing, Verification and Validation (ICST), 2010 Third International Conference on},
 pages={345--354},
 year={2010},
 organization={IEEE}
}
@article{el2006survey,
 title={Survey on the use of formal languages/models for the specification, verification, and enforcement of network access-lists},
 author={El-Atawy, Adel},
 journal={School of Computer Science, Telecommunication, and Information Systems, DePaul University, Chicago, Illinois},
 volume={60604},
 year={2006}
}
@article{pozo2009model,
 title={Model-based development of firewall rule sets: Diagnosing model inconsistencies},
 author={Pozo, S and Ceballos, Rafael and Gasca, Rafael Martinez},
 journal={Information and Software Technology},
 volume={51},
 number={5},
 pages={894--915},
 year={2009},
 publisher={Elsevier}
}
@inproceedings{lopes2015checking,
 title={Checking beliefs in dynamic networks},
 author={Lopes, Nuno P and Bj{\o}rner, Nikolaj and Godefroid, Patrice and Jayaraman, Karthick and Varghese, George},
 booktitle={Proceedings of the 12th USENIX Symposium on Networked Systems Design and Implementation, NSDI},
 volume={15},
 year={2015}
}
@article{anderson2014netkat,
 title={{NetKAT}: Semantic foundations for networks},
 author={Anderson, Carolyn Jane and Foster, Nate and Guha, Arjun and Jeannin, Jean-Baptiste and Kozen, Dexter and Schlesinger, Cole and Walker, David},
 journal={ACM SIGPLAN Notices},
 volume={49},
 number={1},
 pages={113--126},
 year={2014},
 publisher={ACM}
}
@article{mai2011debugging,
 title={Debugging the data plane with anteater},
 author={Mai, Haohui and Khurshid, Ahmed and Agarwal, Rachit and Caesar, Matthew and Godfrey, P and King, Samuel Talmadge},
 journal={ACM SIGCOMM Computer Communication Review},
 volume={41},
 number={4},
 pages={290--301},
 year={2011},
 publisher={ACM}
}
@misc{specification15,
 title={{OpenFlow Switch Specification} V1.5.1},
 month={March},
 year={2015},
}
@misc{specification10,
 title={{OpenFlow Switch Specification} V1.0.0},
 month={December},
 year={2009},
}
@Book{nipkow2002isabelle,
 author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
 title  = {{Isabelle/HOL} --- A Proof Assistant for Higher-Order Logic},
 publisher = {Springer},
 series = {LNCS},
 volume = 2283,
 year = 2015,
}
@inproceedings{canini2012nice,
 title={A {NICE} Way to Test {O}pen{F}low Applications},
 author={Canini, Marco and Venzano, Daniele and Peresini, Peter and Kostic, Dejan and Rexford, Jennifer and others},
 booktitle={NSDI},
 volume={12},
 pages={127--140},
 year={2012}
}
@article{mckeown2008openflow,
 author = {McKeown, Nick and Anderson, Tom and Balakrishnan, Hari and Parulkar, Guru and Peterson, Larry and Rexford, Jennifer and Shenker, Scott and Turner, Jonathan},
 title = {{OpenFlow: Enabling Innovation in Campus Networks}},
 journal = {SIGCOMM Comput. Commun. Rev.},
 issue_date = {April 2008},
 volume = {38},
 number = {2},
 month = {March},
 year = {2008},
 issn = {0146-4833},
 pages = {69--74},
 numpages = {6},
 url = {http://doi.acm.org/10.1145/1355734.1355746},
 doi = {10.1145/1355734.1355746},
 acmid = {1355746},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {ethernet switch, flow-based, virtualization},
}
@article{monsanto2012compiler,
 title={A compiler and run-time system for network programming languages},
 author={Monsanto, Christopher and Foster, Nate and Harrison, Rob and Walker, David},
 journal={ACM SIGPLAN Notices},
 volume={47},
 number={1},
 pages={217--230},
 year={2012},
 publisher={ACM}
}
@inproceedings{kang2013optimizing,
 author = {Kang, Nanxi and Liu, Zhenming and Rexford, Jennifer and Walker, David},
 title = {{Optimizing the "One Big Switch" Abstraction in Software-defined Networks}},
 booktitle = {Proceedings of the Ninth ACM Conference on Emerging Networking Experiments and Technologies},
 series = {CoNEXT '13},
 year = {2013},
 isbn = {978-1-4503-2101-3},
 location = {Santa Barbara, California, USA},
 pages = {13--24},
 numpages = {12},
 url = {http://doi.acm.org.eaccess.ub.tum.de/10.1145/2535372.2535373},
 doi = {10.1145/2535372.2535373},
 acmid = {2535373},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {network virtualization, software-defined networks},
}
@inproceedings{casado2010virtualizing,
 author = {Casado, Mart\'{\i}n and Koponen, Teemu and Ramanathan, Rajiv and Shenker, Scott},
 title = {{Virtualizing the Network Forwarding Plane}},
 booktitle = {Proceedings of the Workshop on Programmable Routers for Extensible Services of Tomorrow},
 series = {PRESTO '10},
 year = {2010},
 isbn = {978-1-4503-0467-2},
 location = {Philadelphia, Pennsylvania},
 pages = {8:1--8:6},
 articleno = {8},
 numpages = {6},
 url = {http://doi.acm.org/10.1145/1921151.1921162},
 doi = {10.1145/1921151.1921162},
 acmid = {1921162},
 publisher = {ACM},
 address = {New York, NY, USA},
}
@inproceedings{monsanto2013composing,
 title={{Composing Software Defined Networks}},
 author={Monsanto, Christopher and Reich, Joshua and Foster, Nate and Rexford, Jennifer and Walker, David and others},
 booktitle={{Networked Systems Design and Implementation}},
 pages={1--13},
 year={2013}
}
@incollection{diekmann2015semantics,
 year={2015},
 isbn={978-3-319-19248-2},
 booktitle={FM 2015: Formal Methods},
 volume={9109},
 series={Lecture Notes in Computer Science},
 editor={Bjørner, Nikolaj and de Boer, Frank},
 doi={10.1007/978-3-319-19249-9_13},
 title={{Semantics-Preserving Simplification of Real-World Firewall Rule Sets}},
 url={https://doi.org/10.1007/978-3-319-19249-9_13},
 publisher={Springer International Publishing},
 keywords={Computer networks; Firewalls; Isabelle; Netfilter Iptables; Semantics},
 author={Diekmann, Cornelius and Hupel, Lars and Carle, Georg},
 pages={195-212},
 language={English}
}
@inproceedings{marmorstein2005tool,
 title={{A Tool for Automated iptables Firewall Analysis}},
 author={Marmorstein, Robert M and Kearns, Phil},
 booktitle={Usenix annual technical conference, Freenix Track},
 pages={71--81},
 year={2005}
}
@misc{openvswitch,
 title={{Open vSwitch}},
 howpublished="\url{http://openvswitch.org/}",
}
@inproceedings{chipounov2009selective,
 title={Selective symbolic execution},
 author={Chipounov, Vitaly and Georgescu, Vlad and Zamfir, Cristian and Candea, George},
 booktitle={Workshop on Hot Topics in Dependable Systems},
 year={2009},
 organization={Citeseer}
}
@unpublished{shenkerfuture,
 title  = {The Future of Networking, and the Past of Protocols},
 author = {Scott Shenker and Martín Casado and Teemu Koponen and Nick McKeown},
 year   = {2011},
 note   = {Talk at Open Networking Summit},
}
@misc{ponemon,
 title = {Study on Datacenter Outages},
 year = {2013},
 author = {{Ponemon Institute LLC}},
 month={September},
}
@book{bidgoli2004internet,
 title={The {I}nternet encyclopedia},
 author={Bidgoli, Hossein},
 volume={3},
 year={2004},
 publisher={John Wiley \& Sons}
}
@ARTICLE{bryant1986graph,
 author={Bryant, R.E.},
 journal={Computers, IEEE Transactions on},
 title={Graph-Based Algorithms for Boolean Function Manipulation},
 year={1986},
 volume={C-35},
 number={8},
 pages={677-691},
 keywords={Boolean functions;binary decision diagrams;logic design verification;symbolic manipulation;Algebra;Application software;Artificial intelligence;Boolean functions;Combinatorial mathematics;Computer science;Data structures;Digital systems;Logic design;Logic testing;Boolean functions;binary decision diagrams;logic design verification;symbolic manipulation},
 doi={10.1109/TC.1986.1676819},
 ISSN={0018-9340},
 month={August},
}
@INPROCEEDINGS{yuan2006fireman,
 author={Lihua Yuan and Hao Chen and Jianning Mai and Chuah, Chen-Nee and Zhendong Su and Mohapatra, P.},
 booktitle={Security and Privacy, 2006 IEEE Symposium on},
 title={FIREMAN: a toolkit for firewall modeling and analysis},
 year={2006},
 pages={15 pp.-213},
 keywords={program diagnostics;security of data;software tools;FIREMAN;binary decision diagrams;distributed firewalls;enterprise networks;firewall analysis;firewall modeling;misconfiguration checking;network security;networked systems;policy violations;static analysis toolkit;symbolic model checking;Boolean functions;Data privacy;Data security;Data structures;Filtering;Hardware;Production;Routing;Telecommunication traffic;Wool},
 doi={10.1109/SP.2006.16},
 ISSN={1081-6011},
 month={May},
}
@article{liaw1992obdd,
 title={On the {OBDD}-representation of general {B}oolean functions},
 author={Liaw, Heh-Tyan and Lin, Chen-Shang},
 journal={IEEE Transactions on computers},
 volume={6},
 pages={661--664},
 year={1992},
 publisher={IEEE}
}
@INPROCEEDINGS{xie2005static,
 author={Xie, G.G. and Jibin Zhan and Maltz, D.A. and Hui Zhang and Greenberg, Albert and Hjalmtysson, G. and Rexford, J.},
 booktitle={INFOCOM 2005. 24th Annual Joint Conference of the IEEE Computer and Communications Societies. Proceedings IEEE},
 title={On static reachability analysis of {IP} networks},
 year={2005},
 volume={3},
 pages={2170-2183 vol. 3},
 keywords={IP networks;computer network reliability;failure analysis;reachability analysis;routing protocols;IP networks;failure analysis;packet filters;packet transformations;routers;routing protocols;static reachability analysis;Bones;Computer networks;Failure analysis;Filters;IP networks;Performance analysis;Probes;Reachability analysis;Routing protocols;Telecommunication traffic},
 doi={10.1109/INFCOM.2005.1498492},
 ISSN={0743-166X},
 month={March},
}
@inproceedings{nelson2014tierless,
 title={Tierless programming and reasoning for software-defined networks},
 author={Nelson, Tim and Ferguson, Andrew D and Scheer, Michael JG and Krishnamurthi, Shriram},
 booktitle={11th USENIX Symposium on Networked Systems Design and Implementation (NSDI 14)},
 pages={519--531},
 year={2014}
}
@incollection{z3,
 year={2008},
 isbn={978-3-540-78799-0},
 booktitle={Tools and Algorithms for the Construction and Analysis of Systems},
 volume={4963},
 series={Lecture Notes in Computer Science},
 editor={Ramakrishnan, C.R. and Rehof, Jakob},
 doi={10.1007/978-3-540-78800-3_24},
 title={{Z3: An Efficient SMT Solver}},
 url={https://doi.org/10.1007/978-3-540-78800-3_24},
 publisher={Springer Berlin Heidelberg},
 author={de Moura, Leonardo and Bjørner, Nikolaj},
 pages={337-340},
 language={English}
}
@inproceedings{diekmann2016verified,
 author={Cornelius Diekmann and Julius Michaelis and Maximilian Haslbeck and Georg Carle},
 title={{V}erified iptables {F}irewall {A}nalysis},
 year={2016},
 month={May},
 booktitle={Proceedings of IFIP Networking 2016 (NETWORKING 16)},
 language={English}
}
@inproceedings{michaelis2016middlebox,
 author={Julius Michaelis and Cornelius Diekmann},
 title={Middlebox Models in Network Verification Research},
 booktitle={Proceedings of the Seminars Future Internet (FI) and Innovative Internet Technologies and Mobile Communications (IITM), Winter Semester 2015/2016},
 year={2016},
 volume={17},
}
@article{barras1997coq,
 title={The Coq proof assistant reference manual: Version 6.1},
 author={Barras, Bruno and Boutin, Samuel and Cornes, Cristina and Courant, Judica{\"e}l and Filliatre, Jean-Christophe and Gimenez, Eduardo and Herbelin, Hugo and Huet, Gerard and Munoz, Cesar and Murthy, Chetan and others},
 year={1997}
}
@inproceedings{casado2007ethane,
 title={Ethane: taking control of the enterprise},
 author={Casado, Martin and Freedman, Michael J and Pettit, Justin and Luo, Jianying and McKeown, Nick and Shenker, Scott},
 booktitle={ACM SIGCOMM Computer Communication Review},
 volume={37},
 number={4},
 pages={1--12},
 year={2007},
 organization={ACM}
}
@inproceedings{casado2006sane,
 title={SANE: A Protection Architecture for Enterprise Networks.},
 author={Casado, Martin and Garfinkel, Tal and Akella, Aditya and Freedman, Michael J and Boneh, Dan and McKeown, Nick and Shenker, Scott},
 booktitle={Usenix Security},
 year={2006}
}
@article{greenberg2005clean,
 title={A clean slate 4D approach to network control and management},
 author={Greenberg, Albert and Hjalmtysson, Gisli and Maltz, David A and Myers, Andy and Rexford, Jennifer and Xie, Geoffrey and Yan, Hong and Zhan, Jibin and Zhang, Hui},
 journal={ACM SIGCOMM Computer Communication Review},
 volume={35},
 number={5},
 pages={41--54},
 year={2005},
 publisher={ACM}
}
@inproceedings{lantz2010network,
 title={A network in a laptop: rapid prototyping for software-defined networks},
 author={Lantz, Bob and Heller, Brandon and McKeown, Nick},
 booktitle={Proceedings of the 9th ACM SIGCOMM Workshop on Hot Topics in Networks},
 pages={19},
 year={2010},
 organization={ACM}
}
  
@article{Iptables_Semantics-AFP,
  author  = {Cornelius Diekmann and Lars Hupel},
  title   = {{I}ptables {S}emantics},
  journal = {Archive of Formal Proofs},
  month   = sep,
  year    = 2016,
  note    = {\url{http://isa-afp.org/entries/Iptables_Semantics.shtml},
            Formal proof development},
  ISSN    = {2150-914x},
}