@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 Brü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},
}
