%% This BibTeX bibliography file was created using BibDesk.
%% http://bibdesk.sourceforge.net/


%% Created for Larry Paulson at 2020-11-13 12:45:07 +0000 


%% Saved with string encoding Unicode (UTF-8) 


@string{lncs = {Lecture Notes in Computer Science}}


@misc{verifiedSATPlan,
	archiveprefix = {arXiv},
	author = {Mohammad Abdulaziz and Friedrich Kurz},
	date-added = {2020-11-13 12:45:04 +0000},
	date-modified = {2020-11-13 12:45:04 +0000},
	eprint = {2010.14648},
	primaryclass = {cs.AI},
	title = {Formally Verified SAT-Based AI Planning},
	year = {2020}}

@techreport{PDDLref,
	author = {Mc{D}ermott, Drew and Ghallab, Malik and Howe, Adele and Knoblock, Craig and Ram, Ashwin and Veloso, Manuela and Weld, Daniel and Wilkins, David},
	institution = {CVC TR-98-003/DCS TR-1165, Yale Center for Computational Vision and Control},
	priority = {2},
	title = {{PDDL: The Planning Domain Definition Language}},
	year = {1998}}

@inproceedings{BiereCCZ99,
	author = {Armin Biere and Alessandro Cimatti and Edmund M. Clarke and Yunshan Zhu},
	booktitle = {{TACAS}},
	pages = {193--207},
	title = {Symbolic Model Checking without {BDDs}},
	year = {1999}}

@inproceedings{KroeningS03,
	author = {Daniel Kroening and Ofer Strichman},
	booktitle = {{VMCAI}},
	pages = {298--309},
	title = {Efficient Computation of Recurrence Diameters},
	year = {2003}}

@inproceedings{Rintanen:Gretton:2013,
	author = {Jussi Rintanen and Charles Orgill Gretton},
	booktitle = {International Joint Conference on Artificial Intelligence},
	title = {Computing Upper Bounds on Lengths of Transition Sequences},
	year = {2013}}

@inproceedings{sievers:etal:12,
	author = {S. Sievers and M. Ortlieb and M. Helmert},
	bibsource = {DBLP, http://dblp.uni-trier.de},
	booktitle = {Proc. 5th Annual Symposium on Combinatorial Search},
	ee = {http://www.aaai.org/ocs/index.php/SOCS/SOCS12/paper/view/5375},
	title = {Efficient Implementation of Pattern Database Heuristics for Classical Planning},
	year = {2012}}

@inproceedings{sang:etal:05,
	author = {T. Sang and P. Beame and H. A. Kautz},
	bibsource = {DBLP, http://dblp.uni-trier.de},
	booktitle = {Proc. 8th International Conference on Theory and Applications of Satisfiability Testing},
	ee = {http://dx.doi.org/10.1007/11499107_17},
	pages = {226--240},
	publisher = {Springer-Verlag},
	title = {Heuristics for Fast Exact Model Counting},
	year = {2005}}

@article{luna:etal:07,
	author = {G. Luna and P. Bello L{\'o}pez and M. C. Gonz{\'a}lez},
	bibsource = {DBLP, http://dblp.uni-trier.de},
	ee = {http://www.engineeringletters.com/issues_v15/issue_2/EL_15_2_11.pdf},
	journal = {Engineering Letters},
	number = {2},
	pages = {250--258},
	title = {New Polynomial Classes for \#2{SAT} Established Via Graph-Topological Structure},
	volume = {15},
	year = {2007}}

@inproceedings{streeter:07,
	author = {M. J. Streeter and S. F. Smith},
	bibsource = {DBLP, http://dblp.uni-trier.de},
	booktitle = {Proc. 17th International Conference on Automated Planning and Scheduling},
	ee = {http://www.aaai.org/Library/ICAPS/2007/icaps07-040.php},
	pages = {312--319},
	publisher = {AAAI Press},
	title = {Using Decision Procedures Efficiently for Optimization},
	year = {2007}}

@article{gimenez:jonsson:12,
	author = {O. Gim{\'e}nez and A. Jonsson},
	bibsource = {DBLP, http://dblp.uni-trier.de},
	ee = {http://dx.doi.org/10.1016/j.artint.2011.12.002},
	journal = {Artificial Intelligence},
	pages = {25--45},
	title = {The influence of k-dependence on the complexity of planning},
	volume = {177-179},
	year = {2012}}

@article{JonssonB98,
	author = {Peter Jonsson and Christer B{\"a}ckstr{\"o}m},
	journal = {Artificial Intelligence},
	number = {1-2},
	pages = {125-176},
	title = {State-Variable Planning Under Structural Restrictions: Algorithms and Complexity},
	volume = {100},
	year = {1998}}

@article{brafman:domshlak:03,
	author = {R. I. Brafman and C. Domshlak},
	bibsource = {DBLP, http://dblp.uni-trier.de},
	ee = {http://dx.doi.org/10.1613/jair.1146},
	journal = {Journal of Artificial Intelligence Research},
	pages = {315--349},
	title = {Structure and Complexity in Planning with Unary Operators},
	volume = {18},
	year = {2003}}

@article{bylander:94,
	author = {T. Bylander},
	bibsource = {DBLP, http://dblp.uni-trier.de},
	ee = {http://dx.doi.org/10.1016/0004-3702(94)90081-7},
	journal = {Artificial Intelligence},
	number = {1-2},
	pages = {165--204},
	title = {The Computational Complexity of Propositional {STRIPS} Planning},
	volume = {69},
	year = {1994}}

@inproceedings{williams:nayak:97,
	author = {Brian C. Williams and P. Pandurang Nayak},
	bibsource = {DBLP, http://dblp.uni-trier.de},
	booktitle = {International Joint Conference on Artificial Intelligence},
	pages = {1178--1185},
	publisher = {Morgan Kaufmann Publishers},
	title = {A Reactive Planner for a Model-based Executive},
	year = {1997}}

@article{knoblock:94,
	author = {C. A. Knoblock},
	bibsource = {DBLP, http://dblp.uni-trier.de},
	ee = {http://dx.doi.org/10.1016/0004-3702(94)90069-8},
	journal = {Artificial Intelligence},
	number = {2},
	pages = {243--302},
	title = {Automatically Generating Abstractions for Planning},
	volume = {68},
	year = {1994}}

@article{rintanen:12,
	author = {Jussi Rintanen},
	bibsource = {DBLP, http://dblp.uni-trier.de},
	ee = {http://dx.doi.org/10.1016/j.artint.2012.08.001},
	journal = {Artificial Intelligence},
	pages = {45--86},
	title = {Planning as satisfiability: Heuristics},
	volume = {193},
	year = {2012}}

@inproceedings{haslum:07,
	author = {Patrik Haslum},
	booktitle = {ICAPS workshop on the IPC: Past, Present and Future},
	title = {Quality of Solutions to {IPC5} Benchmark Problems: Preliminary Results},
	year = {2007}}

@article{Helmert06,
	author = {Malte Helmert},
	journal = {Journal of Artificial Intelligence Research},
	pages = {191-246},
	title = {The {Fast} {Downward} Planning System},
	volume = {26},
	year = {2006}}

@inproceedings{haslum:etal:07,
	author = {P. Haslum and A. Botea and M. Helmert and B. Bonet and S. Koenig},
	bibsource = {DBLP, http://dblp.uni-trier.de},
	booktitle = {Proc 22nd AAAI Conf. on Artificial Intelligence},
	ee = {http://www.aaai.org/Library/AAAI/2007/aaai07-160.php},
	pages = {1007--1012},
	publisher = {AAAI Press},
	title = {Domain-Independent Construction of Pattern Database Heuristics for Cost-Optimal Planning},
	year = {2007}}

@inproceedings{kautz:selman:96,
	author = {H. A. Kautz and B. Selman},
	bibsource = {DBLP, http://dblp.uni-trier.de},
	booktitle = {Proc. 13th National Conf. on Artificial Intelligence},
	ee = {http://www.aaai.org/Library/AAAI/1996/aaai96-177.php},
	pages = {1194--1201},
	publisher = {AAAI Press},
	title = {Pushing the Envelope: Planning, Propositional Logic and Stochastic Search},
	year = {1996}}

@inproceedings{kautz:selman:92,
	author = {H. A. Kautz and B. Selman},
	bibsource = {DBLP, http://dblp.uni-trier.de},
	booktitle = {ECAI},
	pages = {359--363},
	title = {Planning as Satisfiability},
	year = {1992}}

@book{abelson-et-al:scheme,
	address = {Cambridge, Massachusetts},
	author = {Harold Abelson and Gerald~Jay Sussman and Julie Sussman},
	publisher = {MIT Press},
	title = {Structure and Interpretation of Computer Programs},
	year = {1985}}

@inproceedings{HOLsystem,
	author = {Konrad Slind and Michael Norrish},
	booktitle = {TPHOLs},
	title = {A Brief Overview of {HOL4}},
	year = 2008}

@inproceedings{HOLsystemL,
	author = {Konrad Slind and Michael Norrish},
	booktitle = {Theorem Proving in Higher Order Logics},
	pages = {28--32},
	publisher = {Springer},
	series = {LNCS},
	title = {A Brief Overview of {HOL4}},
	volume = 5170,
	year = 2008}

@inproceedings{anonymous,
	author = {Hidden},
	booktitle = {Hidden},
	title = {Title hidden to preserve anonymity.},
	year = {2014}}

@inproceedings{Selman94,
	author = {Selman, Bart},
	booktitle = {KR},
	pages = {521--529},
	title = {Near-optimal plans, tractability, and reactivity},
	year = {1994}}

@article{cooper:etal:11,
	author = {M. C. Cooper and M. de Roquemaurel and P. R{\'e}gnier},
	bibsource = {DBLP, http://dblp.uni-trier.de},
	ee = {http://dx.doi.org/10.3233/AIC-2010-0473},
	journal = {AI Commun.},
	number = {1},
	pages = {1--9},
	title = {A weighted {CSP} approach to cost-optimal planning},
	volume = {24},
	year = {2011}}

@inproceedings{gerevini:schubert:98,
	author = {A. Gerevini and L. K. Schubert},
	bibsource = {DBLP, http://dblp.uni-trier.de},
	booktitle = {Proc. 15th National Conf. on Artificial Intelligence},
	ee = {http://www.aaai.org/Library/AAAI/1998/aaai98-128.php},
	pages = {905--912},
	publisher = {AAAI Press},
	title = {Inferring State Constraints for Domain-Independent Planning},
	year = {1998}}

@article{JonssonBackstrom98b,
	author = {P. Jonsson and C. B{\"a}ckstr{\"o}m},
	bibsource = {DBLP, http://dblp.uni-trier.de},
	ee = {http://dx.doi.org/10.1023/A:1018995620232},
	journal = {Ann. Math. Artificial Intelligence},
	number = {3-4},
	pages = {281--296},
	title = {Tractable Plan Existence Does Not Imply Tractable Plan Generation},
	volume = {22},
	year = {1998}}

@article{hart:etal:68,
	author = {P. E. Hart and N. J. Nilsson and B. Raphael},
	bibsource = {DBLP, http://dblp.uni-trier.de},
	ee = {http://dx.doi.org/10.1109/TSSC.1968.300136},
	journal = {IEEE Trans. Systems Science and Cybernetics},
	number = {2},
	pages = {100--107},
	title = {A Formal Basis for the Heuristic Determination of Minimum Cost Paths},
	volume = {4},
	year = {1968}}

@inproceedings{haslum:geffner:00,
	author = {P. Haslum and H. Geffner},
	bibsource = {DBLP, http://dblp.uni-trier.de},
	booktitle = {Proc. Int. Conf. on AI Planning Systems},
	ee = {http://www.aaai.org/Library/AIPS/2000/aips00-015.php},
	pages = {140--149},
	title = {Admissible Heuristics for Optimal Planning},
	year = {2000}}

@article{drager:etal:09,
	author = {K. Dr{\"a}ger and B. Finkbeiner and A. Podelski},
	bibsource = {DBLP, http://dblp.uni-trier.de},
	ee = {http://dx.doi.org/10.1007/s10009-008-0092-z},
	journal = {STTT},
	number = {1},
	pages = {27--37},
	title = {Directed model checking with distance-preserving abstractions},
	volume = {11},
	year = {2009}}

@article{bonet:geffner:01,
	author = {Blai Bonet and Hector Geffner},
	bibsource = {DBLP, http://dblp.uni-trier.de},
	ee = {http://dx.doi.org/10.1016/S0004-3702(01)00108-4},
	journal = {Artificial Intelligence},
	number = {1-2},
	pages = {5--33},
	title = {Planning as heuristic search},
	volume = {129},
	year = {2001}}

@inproceedings{korf:97,
	author = {R. E. Korf},
	bibsource = {DBLP, http://dblp.uni-trier.de},
	booktitle = {Proc. 14th National Conf. on Artificial Intelligence},
	ee = {http://www.aaai.org/Library/AAAI/1997/aaai97-109.php},
	pages = {700--705},
	publisher = {AAAI Press},
	title = {Finding Optimal Solutions to {R}ubik's Cube Using Pattern Databases},
	year = {1997}}

@inproceedings{culberson:schaeffer:96,
	author = {J. C. Culberson and J. Schaeffer},
	bibsource = {DBLP, http://dblp.uni-trier.de},
	booktitle = {Canadian Conf. on AI},
	ee = {http://dx.doi.org/10.1007/3-540-61291-2_68},
	pages = {402--416},
	publisher = {Springer-Verlag},
	title = {Searching with Pattern Databases},
	year = {1996}}

@article{tarjan:72,
	author = {R. E. Tarjan},
	bibsource = {DBLP, http://dblp.uni-trier.de},
	ee = {http://dx.doi.org/10.1137/0201010},
	journal = {SIAM J. Comput.},
	number = {2},
	pages = {146--160},
	title = {Depth-First Search and Linear Graph Algorithms},
	volume = {1},
	year = {1972}}

@inproceedings{rintanen:08,
	author = {Rintanen, Jussi},
	booktitle = {Proc. 18th European Conf. on AI},
	pages = {568--571},
	publisher = {IOS Press},
	title = {Regression for classical and nondeterministic planning},
	year = 2008}

@inproceedings{rintanen:04,
	author = {Jussi Rintanen},
	bibsource = {DBLP, http://dblp.uni-trier.de},
	booktitle = {Proc. 16th European Conf. on Artificial Intelligence},
	pages = {682--687},
	publisher = {IOS Press},
	title = {Evaluation Strategies for Planning as Satisfiability},
	year = {2004}}

@inproceedings{robinson09,
	author = {Nathan Robinson and Charles Gretton and Duc Nghia Pham and Abdul Sattar},
	booktitle = {ICAPS},
	title = {{SAT}-Based Parallel Planning Using a Split Representation of Actions},
	year = {2009}}

@inproceedings{bgf:Lixto,
	address = {Rome, Italy},
	author = {Robert Baumgartner and Georg Gottlob and Sergio Flesca},
	booktitle = {Proceedings of the 27th Intnl. Conf. on Very Large Databases},
	month = {September},
	pages = {119-128},
	publisher = {Morgan Kaufmann},
	title = {Visual Information Extraction with {Lixto}},
	year = {2001}}

@article{brachman-schmolze:kl-one,
	author = {Ronald~J. Brachman and James~G. Schmolze},
	journal = {Cognitive Science},
	month = {April--June},
	number = {2},
	pages = {171--216},
	title = {An overview of the {KL-ONE} knowledge representation system},
	volume = {9},
	year = {1985}}

@article{gottlob:nonmon,
	author = {Georg Gottlob},
	journal = {Journal of Logic and Computation},
	month = {June},
	number = {3},
	pages = {397--425},
	title = {Complexity results for nonmonotonic logics},
	volume = {2},
	year = {1992}}

@article{gls:hypertrees,
	author = {Georg Gottlob and Nicola Leone and Francesco Scarcello},
	journal = {Journal of Computer and System Sciences},
	month = {May},
	number = {3},
	pages = {579--627},
	title = {Hypertree Decompositions and Tractable Queries},
	volume = {64},
	year = {2002}}

@article{levesque:functional-foundations,
	author = {Hector~J. Levesque},
	journal = {Artificial Intelligence},
	month = {July},
	number = {2},
	pages = {155--212},
	title = {Foundations of a functional approach to knowledge representation},
	volume = {23},
	year = {1984}}

@inproceedings{levesque:belief,
	address = {Austin, Texas},
	author = {Hector~J. Levesque},
	booktitle = {Proceedings of the Fourth National Conf. on Artificial Intelligence},
	month = {August},
	pages = {198--202},
	publisher = {American Association for Artificial Intelligence},
	title = {A logic of implicit and explicit belief},
	year = {1984}}

@article{nebel:jair-2000,
	author = {Bernhard Nebel},
	journal = {Journal of Artificial Intelligence Research},
	pages = {271--315},
	title = {On the compilability and expressive power of propositional planning formalisms},
	volume = {12},
	year = {2000}}

@book{hodges1993model,
	author = {Hodges, Wilfrid},
	publisher = {Cambridge University Press Cambridge},
	title = {Model theory},
	volume = {42},
	year = {1993}}

@book{jackson2006:alloy-book,
	author = {Daniel Jackson},
	bibsource = {dblp computer science bibliography, http://dblp.org},
	biburl = {http://dblp.uni-trier.de/rec/bib/books/daglib/0024034},
	isbn = {978-0-262-10114-1},
	publisher = {{MIT} Press},
	timestamp = {Fri, 20 Oct 4446299 22:18:08 +},
	title = {Software Abstractions: Logic, Language, and Analysis},
	year = {2006}}

@inproceedings{Nipkow-ICTAC06,
	author = {Tobias Nipkow},
	booktitle = {Theoretical Aspects of Computing (ICTAC 2006)},
	editor = {K. Barkaoui and A. Cavalcanti and A. Cerone},
	note = {Invited paper.},
	publisher = {Springer},
	series = LNCS,
	title = {Verifying a Hotel Key Card System},
	volume = 4281,
	year = 2006}

@inproceedings{baumgartner2002property,
	author = {Baumgartner, Jason and Kuehlmann, Andreas and Abraham, Jacob},
	booktitle = {Computer Aided Verification},
	organization = {Springer},
	pages = {151--165},
	title = {Property Checking Via Structural Analysis},
	year = {2002}}

@inproceedings{BlanchetteN10,
	author = {Jasmin Christian Blanchette and Tobias Nipkow},
	bibsource = {dblp computer science bibliography, http://dblp.org},
	booktitle = {Interactive Theorem Proving, First International Conference, {ITP} 2010},
	doi = {10.1007/978-3-642-14052-5_11},
	pages = {131--146},
	title = {Nitpick: {A} Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder},
	year = {2010},
	Bdsk-Url-1 = {https://doi.org/10.1007/978-3-642-14052-5_11}}

@inproceedings{DBLP:conf/date/BaumgartnerK04,
	author = {Jason Baumgartner and Andreas Kuehlmann},
	bibsource = {dblp computer science bibliography, http://dblp.org},
	biburl = {http://dblp.uni-trier.de/rec/bib/conf/date/BaumgartnerK04},
	booktitle = {{DATE} 2004, 16-20 February 2004, Paris, France},
	doi = {10.1109/DATE.2004.1268824},
	pages = {36--41},
	timestamp = {Wed, 26 Oct 2011 12:00:27 +0200},
	title = {Enhanced Diameter Bounding via Structural Analysis},
	year = {2004},
	Bdsk-Url-1 = {https://doi.org/10.1109/DATE.2004.1268824}}

@article{DBLP:journals/ac/BiereCCSZ03,
	author = {Armin Biere and Alessandro Cimatti and Edmund M. Clarke and Ofer Strichman and Yunshan Zhu},
	journal = {Advances in Computers},
	pages = {117--148},
	title = {Bounded model checking},
	volume = {58},
	year = {2003}}

@inproceedings{DBLP:conf/fmcad/SheeranSS00,
	author = {Mary Sheeran and Satnam Singh and Gunnar St{\aa}lmarck},
	bibsource = {dblp computer science bibliography, http://dblp.org},
	biburl = {http://dblp.uni-trier.de/rec/bib/conf/fmcad/SheeranSS00},
	booktitle = {Formal Methods in Computer-Aided Design, Third International Conference, {FMCAD} 2000, Austin, Texas, USA, November 1-3, 2000, Proceedings},
	doi = {10.1007/3-540-40922-X_8},
	pages = {108--125},
	timestamp = {Tue, 21 Jun 2011 16:40:02 +0200},
	title = {Checking Safety Properties Using Induction and a {SAT}-Solver},
	year = {2000},
	Bdsk-Url-1 = {https://doi.org/10.1007/3-540-40922-X_8}}

@inproceedings{DBLP:conf/nca/SastryW14,
	author = {Srikanth Sastry and Josef Widder},
	bibsource = {dblp computer science bibliography, http://dblp.org},
	biburl = {http://dblp.uni-trier.de/rec/bib/conf/nca/SastryW14},
	booktitle = {2014 {IEEE} 13th International Symposium on Network Computing and Applications, {NCA} 2014, Cambridge, MA, USA, 21-23 August, 2014},
	doi = {10.1109/NCA.2014.46},
	pages = {269--276},
	timestamp = {Tue, 25 Nov 2014 17:05:18 +0100},
	title = {Solvability-Based Comparison of Failure Detectors},
	year = {2014},
	Bdsk-Url-1 = {https://doi.org/10.1109/NCA.2014.46}}

@inproceedings{DBLP:conf/date/GanaiG08,
	author = {Malay K. Ganai and Aarti Gupta},
	bibsource = {dblp computer science bibliography, http://dblp.org},
	biburl = {http://dblp.uni-trier.de/rec/bib/conf/date/GanaiG08},
	booktitle = {Design, Automation and Test in Europe, {DATE} 2008, Munich, Germany, March 10-14, 2008},
	doi = {10.1109/DATE.2008.4484777},
	pages = {831--836},
	timestamp = {Mon, 21 Sep 2009 09:13:26 +0200},
	title = {Completeness in {SMT}-based {BMC} for Software Programs},
	year = {2008},
	Bdsk-Url-1 = {https://doi.org/10.1109/DATE.2008.4484777}}

@inproceedings{DBLP:conf/fmcad/CaseMBK09,
	author = {Michael L. Case and Hari Mony and Jason Baumgartner and Robert Kanzelman},
	bibsource = {dblp computer science bibliography, http://dblp.org},
	biburl = {http://dblp.uni-trier.de/rec/bib/conf/fmcad/CaseMBK09},
	booktitle = {{FMCAD} 2009, 15-18 November 2009, Austin, Texas, {USA}},
	pages = {17--24},
	timestamp = {Wed, 27 Jan 2010 15:12:16 +0100},
	title = {Enhanced verification by temporal decomposition},
	year = {2009}}

@article{soares1992maximum,
	author = {Soares, Jos{\'e}},
	journal = {Journal of Graph Theory},
	number = {5},
	pages = {437--450},
	publisher = {Wiley Online Library},
	title = {Maximum diameter of regular digraphs},
	volume = {16},
	year = {1992}}

@article{erdHos1989radius,
	author = {Erd{\H{o}}s, Paul and Pach, Janos and Pollack, Richard and Tuza, Zsolt},
	journal = {Journal of Combinatorial Theory, Series B},
	number = {1},
	pages = {73--79},
	publisher = {Elsevier},
	title = {Radius, diameter, and minimum degree},
	volume = {47},
	year = {1989}}

@article{moon1965diameter,
	author = {Moon, John W and others},
	journal = {The Michigan Mathematical Journal},
	number = {3},
	pages = {349--351},
	publisher = {The University of Michigan},
	title = {On the diameter of a graph.},
	volume = {12},
	year = {1965}}

@article{knyazev1987diameters,
	author = {Knyazev, AV},
	journal = {Mathematical Notes},
	number = {6},
	pages = {473--482},
	publisher = {Springer},
	title = {Diameters of pseudosymmetric graphs},
	volume = {41},
	year = {1987}}

@article{dankelmann2005diameter,
	author = {Dankelmann, Peter},
	journal = {Journal of Combinatorial Theory, Series B},
	number = {1},
	pages = {183--186},
	publisher = {Elsevier},
	title = {The diameter of directed graphs},
	volume = {94},
	year = {2005}}

@article{dankelmann2010diameter,
	author = {Dankelmann, Peter and Volkmann, Lutz},
	journal = {the electronic journal of combinatorics},
	number = {1},
	pages = {R157},
	title = {The diameter of almost Eulerian digraphs},
	volume = {17},
	year = {2010}}

@article{dankelmann2016diameter,
	author = {Dankelmann, Peter and Dorfling, Michael},
	journal = {Discrete Mathematics},
	number = {4},
	pages = {1355--1361},
	publisher = {North-Holland},
	title = {Diameter and maximum degree in Eulerian digraphs},
	volume = {339},
	year = {2016}}

@inproceedings{clarke2001progress,
	author = {Clarke, Edmund and Grumberg, Orna and Jha, Somesh and Lu, Yuan and Veith, Helmut},
	booktitle = {Informatics},
	organization = {Springer},
	pages = {176--194},
	title = {Progress on the state explosion problem in model checking},
	year = {2001}}

@inproceedings{kroening2011linear,
	author = {Kroening, Daniel and Ouaknine, Jo{\"e}l and Strichman, Ofer and Wahl, Thomas and Worrell, James},
	booktitle = {Computer Aided Verification},
	organization = {Springer},
	pages = {557--572},
	title = {Linear completeness thresholds for bounded model checking},
	year = {2011}}

@inproceedings{bundala2012magnitude,
	author = {Bundala, Daniel and Ouaknine, Jo{\"e}l and Worrell, James},
	booktitle = {Proceedings of the 2012 27th Annual IEEE/ACM Symposium on Logic in Computer Science},
	organization = {IEEE Computer Society},
	pages = {155--164},
	title = {On the magnitude of completeness thresholds in bounded model checking},
	year = {2012}}

@article{fikes1971strips,
	author = {Fikes, Richard E and Nilsson, Nils J},
	journal = {Artificial intelligence},
	number = {3-4},
	pages = {189--208},
	publisher = {Elsevier},
	title = {STRIPS: A new approach to the application of theorem proving to problem solving},
	volume = {2},
	year = {1971}}

@incollection{mcmillan1993symbolic,
	author = {McMillan, Kenneth L},
	booktitle = {Symbolic Model Checking},
	pages = {25--60},
	publisher = {Springer},
	title = {Symbolic model checking},
	year = {1993}}

@article{kroening2006computing,
	author = {Kroening, Daniel},
	journal = {Electronic Notes in Theoretical Computer Science},
	number = {1},
	pages = {79--92},
	publisher = {Elsevier},
	title = {Computing over-approximations with bounded model checking},
	volume = {144},
	year = {2006}}

@article{yuster2010computing,
	author = {Yuster, Raphael},
	journal = {arXiv preprint arXiv:1011.6181},
	title = {{Computing the diameter polynomially faster than APSP}},
	year = {2010}}

@article{asgharian2016approximation,
	author = {Asgharian Sardroud, Asghar and Bagheri, Alireza},
	journal = {Optimization Methods and Software},
	number = {3},
	pages = {479--493},
	publisher = {Taylor \& Francis},
	title = {An approximation algorithm for the longest path problem in solid grid graphs},
	volume = {31},
	year = {2016}}

@article{bjorklund2003finding,
	author = {Bj{\"o}rklund, Andreas and Husfeldt, Thore},
	journal = {SIAM Journal on Computing},
	number = {6},
	pages = {1395--1402},
	publisher = {SIAM},
	title = {Finding a path of superlogarithmic length},
	volume = {32},
	year = {2003}}

@inproceedings{bjorklund2004approximating,
	author = {Bj{\"o}rklund, Andreas and Husfeldt, Thore and Khanna, Sanjeev},
	booktitle = {International Colloquium on Automata, Languages, and Programming},
	organization = {Springer},
	pages = {222--233},
	title = {Approximating longest directed paths and cycles},
	year = {2004}}

@article{aingworth1999fast,
	author = {Aingworth, Donald and Chekuri, Chandra and Indyk, Piotr and Motwani, Rajeev},
	journal = {SIAM Journal on Computing},
	number = {4},
	pages = {1167--1181},
	publisher = {SIAM},
	title = {Fast estimation of diameter and shortest paths (without matrix multiplication)},
	volume = {28},
	year = {1999}}

@incollection{berezin1998compositional,
	author = {Berezin, Sergey and Campos, S{\'e}rgio and Clarke, Edmund M},
	booktitle = {Compositionality: The Significant Difference},
	pages = {81--102},
	publisher = {Springer},
	title = {Compositional reasoning in model checking},
	year = {1998}}

@article{alon1997exponent,
	author = {Alon, Noga and Galil, Zvi and Margalit, Oded},
	journal = {Journal of Computer and System Sciences},
	number = {2},
	pages = {255--262},
	publisher = {Elsevier},
	title = {On the exponent of the all pairs shortest path problem},
	volume = {54},
	year = {1997}}

@article{chan2010more,
	author = {Chan, Timothy M},
	journal = {SIAM Journal on Computing},
	number = {5},
	pages = {2075--2089},
	publisher = {SIAM},
	title = {More algorithms for all-pairs shortest paths in weighted graphs},
	volume = {39},
	year = {2010}}

@article{fredman1976new,
	author = {Fredman, Michael L},
	journal = {SIAM Journal on Computing},
	number = {1},
	pages = {83--89},
	publisher = {SIAM},
	title = {New bounds on the complexity of the shortest path problem},
	volume = {5},
	year = {1976}}

@inproceedings{chechik2014better,
	author = {Chechik, Shiri and Larkin, Daniel H and Roditty, Liam and Schoenebeck, Grant and Tarjan, Robert E and Williams, Virginia Vassilevska},
	booktitle = {Proceedings of the Twenty-Fifth Annual ACM-SIAM Symposium on Discrete Algorithms},
	organization = {Society for Industrial and Applied Mathematics},
	pages = {1041--1052},
	title = {Better approximation algorithms for the graph diameter},
	year = {2014}}

@inproceedings{roditty2013fast,
	author = {Roditty, Liam and Vassilevska Williams, Virginia},
	booktitle = {Proceedings of the forty-fifth annual ACM symposium on Theory of computing},
	organization = {ACM},
	pages = {515--524},
	title = {Fast approximation algorithms for the diameter and radius of sparse graphs},
	year = {2013}}

@inproceedings{abboud2016approximation,
	author = {Abboud, Amir and Williams, Virginia Vassilevska and Wang, Joshua},
	booktitle = {Proceedings of the twenty-seventh annual ACM-SIAM symposium on Discrete Algorithms},
	organization = {SIAM},
	pages = {377--391},
	title = {Approximation and fixed parameter subquadratic algorithms for radius and diameter in sparse graphs},
	year = {2016}}

@article{alon1995color,
	author = {Alon, Noga and Yuster, Raphael and Zwick, Uri},
	journal = {Journal of the ACM (JACM)},
	number = {4},
	pages = {844--856},
	publisher = {ACM},
	title = {Color-coding},
	volume = {42},
	year = {1995}}

@article{bulterman2002computing,
	author = {Bulterman, RW and van der Sommen, FW and Zwaan, Gerard and Verhoeff, Tom and van Gasteren, AJM and Feijen, WHJ},
	journal = {Information Processing Letters},
	number = {2},
	pages = {93--96},
	publisher = {Elsevier North-Holland, Inc.},
	title = {On computing a longest path in a tree},
	volume = {81},
	year = {2002}}

@article{gutin1993finding,
	author = {Gutin, Gregory},
	journal = {SIAM Journal on Discrete Mathematics},
	number = {2},
	pages = {270--273},
	publisher = {SIAM},
	title = {Finding a longest path in a complete multipartite digraph},
	volume = {6},
	year = {1993}}

@article{clarke2009turing,
	author = {Clarke, Edmund M and Emerson, E Allen and Sifakis, Joseph},
	journal = {Communications of the ACM},
	number = {11},
	pages = {74--84},
	title = {Turing lecture: model checking--algorithmic verification and debugging},
	volume = {52},
	year = {2009}}

@inproceedings{knoblock1991characterizing,
	author = {Knoblock, Craig A and Tenenberg, Josh D and Yang, Qiang},
	booktitle = {AAAI},
	pages = {692--697},
	title = {Characterizing Abstraction Hierarchies for Planning.},
	year = {1991}}

@inproceedings{clarke2000counterexample,
	author = {Clarke, Edmund and Grumberg, Orna and Jha, Somesh and Lu, Yuan and Veith, Helmut},
	booktitle = {International Conference on Computer Aided Verification},
	organization = {Springer},
	pages = {154--169},
	title = {Counterexample-guided abstraction refinement},
	year = {2000}}

@article{sacerdoti1974planning,
	author = {Sacerdoti, Earl D},
	journal = {Artificial intelligence},
	number = {2},
	pages = {115--135},
	publisher = {Elsevier},
	title = {Planning in a hierarchy of abstraction spaces},
	volume = {5},
	year = {1974}}

@article{seippfast,
	author = {Seipp, Jendrik and Pommerening, Florian and Sievers, Silvan and Wehrle, Martin and Fawcett, Chris and Alkhazraji, Yusra},
	title = {{Fast Downward Aidos}}}

@inproceedings{clarke2004completeness,
	author = {Clarke, Edmund and Kroening, Daniel and Ouaknine, Jo{\"e}l and Strichman, Ofer},
	booktitle = {International Workshop on Verification, Model Checking, and Abstract Interpretation},
	organization = {Springer},
	pages = {85--96},
	title = {Completeness and complexity of bounded model checking},
	year = {2004}}

@inproceedings{uehara2004efficient,
	author = {Uehara, Ryuhei and Uno, Yushi},
	booktitle = {International Symposium on Algorithms and Computation},
	organization = {Springer},
	pages = {871--883},
	title = {Efficient algorithms for the longest path problem},
	year = {2004}}

@inproceedings{porco2013automatic,
	author = {Porco, Aldo and Machado, Alejandro and Bonet, Blai},
	booktitle = {ICAPS},
	title = {Automatic Reductions from {PH} into {STRIPS} or How to Generate Short Problems with Very Long Solutions.},
	year = {2013}}

@article{BrownFP96,
	author = {Cynthia A. Brown and Larry Finkelstein and Paul Walton Purdom Jr.},
	bibsource = {dblp computer science bibliography, http://dblp.org},
	biburl = {http://dblp.uni-trier.de/rec/bib/journals/njc/BrownFP96},
	journal = {Nord. J. Comput.},
	number = {3},
	pages = {203--219},
	timestamp = {Mon, 24 Jul 2006 10:22:32 +0200},
	title = {Backtrack Searching in the Presence of Symmetry},
	volume = {3},
	year = {1996}}

@inproceedings{DeMoura:2008:ZES:1792734.1792766,
	author = {De Moura, Leonardo and Bj{\o}rner, Nikolaj},
	booktitle = {Proc. TACAS'08/ETAPS'08},
	location = {Budapest, Hungary},
	pages = {337--340},
	title = {Z3: An Efficient SMT Solver},
	year = {2008}}

@article{McKay201494,
	author = {Brendan D. McKay and Adolfo Piperno},
	doi = {http://dx.doi.org/10.1016/j.jsc.2013.09.003},
	issn = {0747-7171},
	journal = {Journal of Symbolic Computation},
	number = {0},
	pages = {94 - 112},
	title = {Practical graph isomorphism, \{II\}},
	url = {http://www.sciencedirect.com/science/article/pii/S0747717113001193},
	volume = {60},
	year = {2014},
	Bdsk-Url-1 = {http://www.sciencedirect.com/science/article/pii/S0747717113001193},
	Bdsk-Url-2 = {http://dx.doi.org/10.1016/j.jsc.2013.09.003}}

@article{richter2010lama,
	author = {Richter, Silvia and Westphal, Matthias},
	journal = {Journal of Artificial Intelligence Research},
	number = {1},
	pages = {127--177},
	title = {The {LAMA} Planner: Guiding Cost-based Anytime Planning with Landmarks},
	volume = {39},
	year = {2010}}

@inproceedings{shleyfman2015heuristics,
	author = {Shleyfman, Alexander and Katz, Michael and Helmert, Malte and Sievers, Silvan and Wehrle, Martin},
	booktitle = {AAAI},
	title = {Heuristics and Symmetries in Classical Planning},
	year = {2015}}

@inproceedings{DomshlakKS13,
	author = {Carmel Domshlak and Michael Katz and Alexander Shleyfman},
	booktitle = {ICAPS},
	title = {Symmetry Breaking: Satisficing Planning and Landmark Heuristics},
	year = {2013}}

@article{helmert2014merge,
	author = {Helmert, Malte and Haslum, Patrik and Hoffmann, J{\"o}rg and Nissim, Raz},
	journal = {Journal of the ACM (JACM)},
	number = {3},
	pages = {16},
	publisher = {ACM},
	title = {Merge-and-shrink abstraction: A method for generating lower bounds in factored state spaces},
	volume = {61},
	year = {2014}}

@inproceedings{amir2003factored,
	author = {Amir, Eyal and Engelhardt, Barbara},
	booktitle = {IJCAI},
	organization = {Citeseer},
	pages = {929--935},
	title = {Factored planning},
	volume = {3},
	year = {2003}}

@inproceedings{brafman2006factored,
	author = {Brafman, Ronen I and Domshlak, Carmel},
	booktitle = {AAAI},
	pages = {809--814},
	title = {Factored planning: How, when, and when not},
	volume = {6},
	year = {2006}}

@inproceedings{kelareva2007factored,
	author = {Kelareva, Elena and Buffet, Olivier and Huang, Jinbo and Thi{\'e}baux, Sylvie},
	booktitle = {IJCAI},
	pages = {1942--1947},
	title = {Factored Planning Using Decomposition Trees.},
	year = {2007}}

@inproceedings{sievers:2015,
	author = {Silvan Sievers and Martin Wehrle and Malte Helmert and Alexander Shleyfman and Michael Katz},
	booktitle = {Proc. 29th National Conf. on Artificial Intelligence},
	publisher = {AAAI Press},
	title = {Factored Symmetries for Merge-and-Shrink Abstractions},
	year = {2015}}

@article{crawford1996symmetry,
	author = {Crawford, James and Ginsberg, Matthew and Luks, Eugene and Roy, Amitabha},
	journal = {KR},
	pages = {148--159},
	title = {Symmetry-breaking predicates for search problems},
	volume = {96},
	year = {1996}}

@inproceedings{GuereA01,
	author = {Emmanuel Guere and Rachid Alami},
	bibsource = {dblp computer science bibliography, http://dblp.org},
	biburl = {http://dblp.uni-trier.de/rec/bib/conf/ijcai/GuereA01},
	booktitle = {Proceedings of the Seventeenth International Joint Conference on Artificial Intelligence, {IJCAI} 2001, Seattle, Washington, USA, August 4-10, 2001},
	pages = {439--444},
	timestamp = {Mon, 20 Apr 2009 09:38:06 +0200},
	title = {One action is enough to plan},
	year = {2001}}

@inproceedings{JoslinR97,
	author = {David Joslin and Amitabha Roy},
	bibsource = {dblp computer science bibliography, http://dblp.org},
	biburl = {http://dblp.uni-trier.de/rec/bib/conf/aaai/JoslinR97},
	booktitle = {Proceedings of the Fourteenth National Conference on Artificial Intelligence and Ninth Innovative Applications of Artificial Intelligence Conference, {AAAI} 97, {IAAI} 97, July 27-31, 1997, Providence, Rhode Island.},
	pages = {197--202},
	timestamp = {Tue, 11 Dec 2012 12:57:22 +0100},
	title = {Exploiting Symmetry in Lifted {CSPs}},
	year = {1997}}

@inproceedings{rintanen2003symmetry,
	author = {Rintanen, Jussi},
	booktitle = {ICAPS},
	pages = {32--41},
	title = {Symmetry Reduction for {SAT} Representations of Transition Systems.},
	year = {2003}}

@inproceedings{domshlak2012enhanced,
	author = {Domshlak, Carmel and Katz, Michael and Shleyfman, Alexander},
	booktitle = {ICAPS},
	title = {Enhanced Symmetry Breaking in Cost-Optimal Planning as Forward Search.},
	year = {2012}}

@inproceedings{pochter2011exploiting,
	author = {Pochter, Nir and Zohar, Aviv and Rosenschein, Jeffrey S},
	booktitle = {AAAI},
	title = {Exploiting Problem Symmetries in State-Based Planners.},
	year = {2011}}

@article{WahlD10,
	author = {Thomas Wahl and Alastair F. Donaldson},
	bibsource = {dblp computer science bibliography, http://dblp.org},
	biburl = {http://dblp.uni-trier.de/rec/bib/journals/symmetry/WahlD10},
	doi = {10.3390/sym2020799},
	journal = {Symmetry},
	number = {2},
	pages = {799--847},
	timestamp = {Mon, 21 Feb 2011 21:51:20 +0100},
	title = {Replication and Abstraction: Symmetry in Automated Formal Verification},
	url = {http://dx.doi.org/10.3390/sym2020799},
	volume = {2},
	year = {2010},
	Bdsk-Url-1 = {http://dx.doi.org/10.3390/sym2020799}}

@inproceedings{FoxL99,
	author = {Maria Fox and Derek Long},
	bibsource = {dblp computer science bibliography, http://dblp.org},
	biburl = {http://dblp.uni-trier.de/rec/bib/conf/ijcai/FoxL99},
	booktitle = {Proceedings of the Sixteenth International Joint Conference on Artificial Intelligence, {IJCAI} 99, Stockholm, Sweden, July 31 - August 6, 1999. 2 Volumes, 1450 pages},
	pages = {956--961},
	title = {The Detection and Exploitation of Symmetry in Planning Problems},
	year = {1999}}

@inproceedings{FoxL02,
	author = {Maria Fox and Derek Long},
	booktitle = {Proceedings of the Sixth International Conference on Artificial Intelligence Planning Systems, April 23-27, 2002, Toulouse, France},
	pages = {83--91},
	title = {Extending the Exploitation of Symmetries in Planning},
	year = {2002}}

@article{helmert2006fast,
	author = {Helmert, Malte},
	journal = {J. Artif. Intell. Res.(JAIR)},
	pages = {191--246},
	title = {The Fast Downward Planning System.},
	volume = {26},
	year = {2006}}

@inproceedings{miguel2001symmetry,
	author = {Miguel, Ian},
	booktitle = {{Proceedings of the CP'01 Workshop on Symmetry in Constraints}},
	pages = {17--24},
	title = {Symmetry-breaking in planning: Schematic constraints},
	year = {2001}}

@incollection{Walsh:07,
	author = {Walsh, Toby},
	booktitle = {Principles and Practice of Constraint Programming -- CP 2007},
	doi = {10.1007/978-3-540-74970-7_67},
	editor = {Bessi{\`e}re, Christian},
	isbn = {978-3-540-74969-1},
	language = {English},
	pages = {880-887},
	publisher = {Springer Berlin Heidelberg},
	series = {Lecture Notes in Computer Science},
	title = {Breaking Value Symmetry},
	url = {http://dx.doi.org/10.1007/978-3-540-74970-7_67},
	volume = {4741},
	year = {2007},
	Bdsk-Url-1 = {http://dx.doi.org/10.1007/978-3-540-74970-7_67}}

@inproceedings{eugene1993permutation,
	author = {Eugene, M},
	booktitle = {Groups and Computation: Workshop on Groups and Computation, October 7-10, 1991},
	organization = {American Mathematical Soc.},
	pages = {139},
	title = {Permutation groups and polynomial-time computation},
	volume = {11},
	year = {1993}}

@inproceedings{Babai:1983:CLG:800061.808746,
	acmid = {808746},
	address = {New York, NY, USA},
	author = {Babai, L\'{a}szl\'{o} and Luks, Eugene M.},
	booktitle = {Proceedings of the Fifteenth Annual ACM Symposium on Theory of Computing},
	doi = {10.1145/800061.808746},
	isbn = {0-89791-099-0},
	numpages = {13},
	pages = {171--183},
	publisher = {ACM},
	series = {STOC '83},
	title = {Canonical Labeling of Graphs},
	url = {http://doi.acm.org/10.1145/800061.808746},
	year = {1983},
	Bdsk-Url-1 = {http://doi.acm.org/10.1145/800061.808746},
	Bdsk-Url-2 = {https://doi.org/10.1145/800061.808746}}

@inproceedings{clarke1998symmetry,
	author = {Clarke, Edmund M and Emerson, E Allen and Jha, Somesh and Sistla, A Prasad},
	booktitle = {Computer Aided Verification},
	organization = {Springer},
	pages = {147--158},
	title = {Symmetry reductions in model checking},
	year = {1998}}

@article{bellman1958routing,
	author = {Bellman, Richard},
	journal = {Quarterly of applied mathematics},
	pages = {87--90},
	publisher = {JSTOR},
	title = {On a routing problem},
	year = {1958}}

@article{dijkstra1959note,
	author = {Dijkstra, Edsger W},
	journal = {Numerische mathematik},
	number = {1},
	pages = {269--271},
	publisher = {Springer},
	title = {A note on two problems in connexion with graphs},
	volume = {1},
	year = {1959}}

@article{fredman1987fibonacci,
	author = {Fredman, Michael L and Tarjan, Robert Endre},
	journal = {Journal of the ACM (JACM)},
	number = {3},
	pages = {596--615},
	publisher = {ACM},
	title = {Fibonacci heaps and their uses in improved network optimization algorithms},
	volume = {34},
	year = {1987}}

@inproceedings{thorup2003integer,
	author = {Thorup, Mikkel},
	booktitle = {Proceedings of the thirty-fifth annual ACM symposium on Theory of computing},
	organization = {ACM},
	pages = {149--158},
	title = {Integer priority queues with decrease key in constant time and the single source shortest paths problem},
	year = {2003}}

@article{dufourd2009intuitionistic,
	author = {Dufourd, Jean-Fran{\c{c}}ois},
	journal = {Journal of Automated Reasoning},
	number = {1},
	pages = {19--51},
	publisher = {Springer},
	title = {{An intuitionistic proof of a discrete form of the Jordan Curve Theorem formalized in Coq with combinatorial hypermaps}},
	volume = {43},
	year = {2009}}

@article{bezem2008mechanization,
	author = {Bezem, Marc and Hendriks, Dimitri},
	journal = {Journal of Automated Reasoning},
	number = {1},
	pages = {61--85},
	publisher = {Springer},
	title = {{On the mechanization of the proof of Hessenberg's theorem in coherent logic}},
	volume = {40},
	year = {2008}}

@article{mckinna1999some,
	author = {McKinna, James and Pollack, Robert},
	journal = {Journal of Automated Reasoning},
	number = {3},
	pages = {373--409},
	publisher = {Springer},
	title = {Some lambda calculus and type theory formalized},
	volume = {23},
	year = {1999}}

@inproceedings{taylor1991fixed,
	author = {Taylor, Paul},
	booktitle = {Logic in Computer Science, 1991. LICS'91., Proceedings of Sixth Annual IEEE Symposium on},
	organization = {IEEE},
	pages = {152--160},
	title = {The fixed point property in synthetic domain theory},
	year = {1991}}

@article{jaume1999full,
	author = {Jaume, Mathieu},
	journal = {Journal of Automated Reasoning},
	number = {3},
	pages = {347--371},
	publisher = {Springer},
	title = {A full formalization of SLD-resolution in the Calculus of Inductive Constructions},
	volume = {23},
	year = {1999}}

@article{kamareddine2003formalizing,
	author = {Kamareddine, Fairouz and Qiao, Haiyan},
	journal = {Journal of Automated Reasoning},
	number = {1},
	pages = {59--98},
	publisher = {Springer},
	title = {Formalizing strong normalization proofs of explicit substitution calculi in ALF},
	volume = {30},
	year = {2003}}

@article{manolios2005ordinal,
	author = {Manolios, Panagiotis and Vroon, Daron},
	journal = {Journal of Automated Reasoning},
	number = {4},
	pages = {387--423},
	publisher = {Springer},
	title = {Ordinal arithmetic: Algorithms and mechanization},
	volume = {34},
	year = {2005}}

@article{maric2009formalization,
	author = {Mari{\'c}, Filip},
	journal = {Journal of Automated Reasoning},
	number = {1},
	publisher = {Springer},
	title = {{Formalization and implementation of modern SAT solvers}},
	volume = {43},
	year = {2009}}

@inproceedings{klein2009sel4L,
	author = {Klein, Gerwin and Elphinstone, Kevin and Heiser, Gernot and Andronick, June and Cock, David and Derrin, Philip and Elkaduwe, Dhammika and Engelhardt, Kai and Kolanski, Rafal and Norrish, Michael and others},
	booktitle = {Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles},
	organization = {ACM},
	pages = {207--220},
	title = {{seL4: Formal verification of an OS kernel}},
	year = {2009}}

@inproceedings{klein2009sel4,
	author = {Klein, Gerwin and others},
	booktitle = {SOSP},
	organization = {ACM},
	pages = {207--220},
	title = {{seL4: Formal verification of an OS kernel}},
	year = {2009}}

@book{gordon1993introduction,
	author = {Gordon, Michael JC and Melham, Tom F},
	publisher = {Cambridge University Press},
	title = {Introduction to HOL: a theorem proving environment for higher order logic},
	year = {1993}}

@incollection{bauer2013tableaux,
	author = {Bauer, Andreas and Baumgartner, Peter and Diller, Martin and Norrish, Michael},
	booktitle = {Automated Reasoning with Analytic Tableaux and Related Methods},
	pages = {28--43},
	publisher = {Springer},
	title = {Tableaux for verification of data-centric processes},
	year = {2013}}

@book{paulson1994isabelle,
	author = {Paulson, Lawrence C},
	publisher = {Springer},
	title = {Isabelle: A generic theorem prover},
	volume = {828},
	year = {1994}}

@book{bertot2004interactive,
	author = {Bertot, Yves and Cast{\'e}ran, Pierre},
	publisher = {springer},
	title = {Interactive theorem proving and program development: Coq'Art: the calculus of inductive constructions},
	year = {2004}}

@article{gonthier2008formal,
	author = {Gonthier, Georges},
	journal = {Notices of the AMS},
	number = {11},
	pages = {1382--1393},
	title = {Formal proof--the four-color theorem},
	volume = {55},
	year = {2008}}

@incollection{hales2011revision,
	author = {Hales, Thomas C and Harrison, John and McLaughlin, Sean and Nipkow, Tobias and Obua, Steven and Zumkeller, Roland},
	booktitle = {The Kepler Conjecture},
	pages = {341--376},
	publisher = {Springer},
	title = {{A revision of the proof of the Kepler conjecture}},
	year = {2011}}

@article{gamboa2009formalization,
	author = {Gamboa, Ruben A},
	journal = {Journal of Automated Reasoning},
	number = {2},
	pages = {139--172},
	publisher = {Springer},
	title = {A Formalization of Powerlist Algebra in ACL2},
	volume = {43},
	year = {2009}}

@article{harrison2007formalizing,
	author = {Harrison, John},
	journal = {From Insight to Proof: Festschrift in Honour of Andrzej Trybulec. Studies in Logic, Grammar and Rhetoric},
	number = {23},
	pages = {151--165},
	title = {Formalizing basic complex analysis},
	volume = {10},
	year = {2007}}

@inproceedings{esparza2013fully,
	author = {Esparza, Javier and Lammich, Peter and Neumann, Ren{\'e} and Nipkow, Tobias and Schimpf, Alexander and Smaus, Jan-Georg},
	booktitle = {International Conference on Computer Aided Verification},
	organization = {Springer},
	pages = {463--478},
	title = {{A fully verified executable LTL model checker}},
	year = {2013}}

@inproceedings{paulson2015formalisation,
	author = {Paulson, Lawrence C},
	booktitle = {International Conference on Automated Deduction},
	organization = {Springer},
	pages = {231--245},
	title = {A formalisation of finite automata using hereditarily finite sets},
	year = {2015}}

@inproceedings{constable2000constructively,
	author = {Constable, Robert L and Jackson, Paul B and Naumov, Pavel and Uribe, Juan C},
	booktitle = {Proof, language, and interaction},
	pages = {213--238},
	title = {Constructively formalizing automata theory.},
	year = {2000}}

@inproceedings{doczkal2013constructive,
	author = {Doczkal, Christian and Kaiser, Jan-Oliver and Smolka, Gert},
	booktitle = {International Conference on Certified Programs and Proofs},
	organization = {Springer},
	pages = {82--97},
	title = {A constructive theory of regular languages in Coq},
	year = {2013}}

@inproceedings{wu2011formalisation,
	author = {Wu, Chunhan and Zhang, Xingyuan and Urban, Christian},
	booktitle = {International Conference on Interactive Theorem Proving},
	organization = {Springer},
	pages = {341--356},
	title = {{A formalisation of the Myhill-Nerode theorem based on regular expressions (proof pearl)}},
	year = {2011}}

@inproceedings{schimpf2009construction,
	author = {Schimpf, Alexander and Merz, Stephan and Smaus, Jan-Georg},
	booktitle = {International Conference on Theorem Proving in Higher Order Logics},
	organization = {Springer},
	pages = {424--439},
	title = {{Construction of B{\"u}chi automata for LTL model checking verified in Isabelle/HOL}},
	year = {2009}}

@inproceedings{sprenger1998verified,
	author = {Sprenger, Christoph},
	booktitle = {International Conference on Tools and Algorithms for the Construction and Analysis of Systems},
	organization = {Springer},
	pages = {167--183},
	title = {A verified model checker for the modal $\mu$-calculus in Coq},
	year = {1998}}

@inproceedings{nipkow2005proof,
	author = {Nipkow, Tobias and Paulson, Lawrence C},
	booktitle = {International Conference on Theorem Proving in Higher Order Logics},
	organization = {Springer},
	pages = {385--396},
	title = {Proof pearl: Defining functions over finite sets},
	year = {2005}}

@article{sistla1985complexity,
	author = {Sistla, A Prasad and Clarke, Edmund M},
	journal = {Journal of the ACM (JACM)},
	number = {3},
	pages = {733--749},
	publisher = {ACM},
	title = {The complexity of propositional linear temporal logics},
	volume = {32},
	year = {1985}}

@article{clarke1994model,
	author = {Clarke, Edmund M and Grumberg, Orna and Long, David E},
	journal = {ACM transactions on Programming Languages and Systems (TOPLAS)},
	number = {5},
	pages = {1512--1542},
	publisher = {ACM},
	title = {Model checking and abstraction},
	volume = {16},
	year = {1994}}

@article{filiot2011antichains,
	author = {Filiot, Emmanuel and Jin, Naiyong and Raskin, Jean-Fran{\c{c}}ois},
	journal = {Formal Methods in System Design},
	number = {3},
	pages = {261--296},
	publisher = {Springer},
	title = {{Antichains and compositional algorithms for LTL synthesis}},
	volume = {39},
	year = {2011}}

@inproceedings{abdulaziz2014mechanising,
	author = {Abdulaziz, Mohammad and Gretton, Charles and Norrish, Michael},
	booktitle = {{Workshop on Knowledge Engineering for Planning and Scheduling}},
	title = {{Mechanising Theoretical Upper Bounds in Planning}},
	year = {2014}}

@inproceedings{abdulaziz2015exploiting,
	author = {Abdulaziz, Mohammad and Norrish, Michael and Gretton, Charles},
	booktitle = {{Proc. of the 24th International Joint Conference on Artificial Intelligence, IJCAI}},
	pages = {25--31},
	title = {{Exploiting symmetries by planning for a descriptive quotient}},
	year = {2015}}

@inproceedings{abdulaziz2016isabelle,
	author = {Abdulaziz, Mohammad and Paulson, Lawrence C},
	booktitle = {{International Conference on Interactive Theorem Proving}},
	organization = {Springer},
	pages = {3--19},
	title = {{An Isabelle/HOL formalisation of Green's theorem}},
	year = {2016}}

@incollection{abdulaziz2015verified,
	author = {Abdulaziz, Mohammad and Gretton, Charles and Norrish, Michael},
	booktitle = {{Interactive Theorem Proving}},
	pages = {1--16},
	publisher = {Springer},
	title = {{Verified Over-Approximation of the Diameter of Propositionally Factored Transition Systems}},
	year = {2015}}

@inproceedings{icaps2017,
	author = {Abdulaziz, Mohammad and Gretton, Charles and Norrish, Michael},
	booktitle = {International Conference on Automated Planning and Scheduling (ICAPS)},
	organization = {AAAI},
	title = {{A State Space Acyclicity Property for Exponentially Tighter Plan Length Bounds}},
	year = {2017}}

@article{DBLP:journals/jar/AbdulazizNG18,
	author = {Mohammad Abdulaziz and Michael Norrish and Charles Gretton},
	bibsource = {dblp computer science bibliography, https://dblp.org},
	biburl = {https://dblp.org/rec/bib/journals/jar/AbdulazizNG18},
	journal = {J. Autom. Reasoning},
	number = {1-4},
	pages = {485--520},
	timestamp = {Sat, 02 Jun 2018 16:55:32 +0200},
	title = {{Formally Verified Algorithms for Upper-Bounding State Space Diameters}},
	volume = {61},
	year = {2018}}

@article{pardalos2004note,
	author = {Pardalos, Panos M and Migdalas, Athanasios},
	journal = {Applied mathematics letters},
	number = {1},
	pages = {13--15},
	publisher = {Elsevier},
	title = {A note on the complexity of longest path problems related to graph coloring},
	volume = {17},
	year = {2004}}

@article{galperin1983succinct,
	author = {Galperin, Hana and Wigderson, Avi},
	journal = {Information and Control},
	number = {3},
	pages = {183--198},
	publisher = {Elsevier},
	title = {Succinct representations of graphs},
	volume = {56},
	year = {1983}}

@inproceedings{feigenbaum1998complexity,
	author = {Feigenbaum, Joan and Kannan, Sampath and Vardi, Moshe Y and Viswanathan, Mahesh},
	booktitle = {Annual Symposium on Theoretical Aspects of Computer Science},
	organization = {Springer},
	pages = {216--226},
	title = {Complexity of problems on graphs represented as OBDDs},
	year = {1998}}

@article{hemaspaandra2010complexity,
	author = {Hemaspaandra, Edith and Hemaspaandra, Lane A and Tantau, Till and Watanabe, Osamu},
	journal = {Theoretical Computer Science},
	number = {4-5},
	pages = {783--798},
	publisher = {Elsevier},
	title = {On the complexity of kings},
	volume = {411},
	year = {2010}}

@inproceedings{lozano1989complexity,
	author = {Lozano, Antonio and Balc{\'a}zar, Jos{\'e} L},
	booktitle = {International Workshop on Graph-Theoretic Concepts in Computer Science},
	organization = {Springer},
	pages = {277--286},
	title = {The complexity of graph problems for succinctly represented graphs},
	year = {1989}}

@article{papadimitriou1986note,
	author = {Papadimitriou, Christos H and Yannakakis, Mihalis},
	journal = {Information and Control},
	number = {3},
	pages = {181--185},
	publisher = {Elsevier},
	title = {A note on succinct representations of graphs},
	volume = {71},
	year = {1986}}

@inproceedings{howey2004val,
	author = {Howey, Richard and Long, Derek and Fox, Maria},
	booktitle = {Tools with Artificial Intelligence, 2004},
	title = {{VAL: Automatic plan validation, continuous effects and mixed initiative planning using PDDL}},
	year = {2004}}

@inproceedings{howey2004valL,
	author = {Howey, Richard and Long, Derek and Fox, Maria},
	booktitle = {Tools with Artificial Intelligence, 2004. ICTAI 2004. 16th IEEE International Conference on},
	organization = {IEEE},
	pages = {294--301},
	title = {{VAL: Automatic plan validation, continuous effects and mixed initiative planning using PDDL}},
	year = {2004}}

@article{leroy2009formal,
	author = {Leroy, Xavier},
	journal = {Communications of the ACM},
	number = {7},
	pages = {107--115},
	publisher = {ACM},
	title = {Formal verification of a realistic compiler},
	volume = {52},
	year = {2009}}

@article{fox2003pddl2,
	author = {Fox, Maria and Long, Derek},
	journal = {JAIR},
	title = {{PDDL2.1: An extension to PDDL for expressing temporal planning domains}},
	year = {2003}}

@article{fox2003pddl2L,
	author = {Fox, Maria and Long, Derek},
	journal = {Journal of artificial intelligence research},
	title = {{PDDL2.1: An extension to PDDL for expressing temporal planning domains}},
	year = {2003}}

@inproceedings{fox2005validating,
	author = {Fox, Maria and Howey, Richard and Long, Derek},
	booktitle = {AAAI},
	pages = {1151--1156},
	title = {Validating plans in the context of processes and exogenous events},
	volume = {5},
	year = {2005}}

@inproceedings{brunner2016formal,
	author = {Brunner, Julian and Lammich, Peter},
	booktitle = {NASA Formal Methods Symposium},
	organization = {Springer},
	pages = {307--321},
	title = {{Formal Verification of an Executable LTL Model Checker with Partial Order Reduction}},
	year = {2016}}

@article{holzmann1997model,
	author = {Holzmann, Gerard J.},
	journal = {IEEE Transactions on software engineering},
	number = {5},
	pages = {279--295},
	publisher = {IEEE},
	title = {The model checker SPIN},
	volume = {23},
	year = {1997}}

@book{norell2007towards,
	author = {Norell, Ulf},
	publisher = {Chalmers University of Technology},
	title = {Towards a practical programming language based on dependent type theory},
	volume = {32},
	year = {2007}}

@article{coquand1988calculus,
	author = {Coquand, Thierry and Huet, G{\'e}rard},
	journal = {Information and computation},
	number = {2-3},
	pages = {95--120},
	publisher = {Elsevier},
	title = {The calculus of constructions},
	volume = {76},
	year = {1988}}

@article{haftmann2007code,
	author = {Haftmann, Florian and Nipkow, Tobias},
	journal = {Theorem Proving in Higher Order Logics (TPHOLs 2007). Lecture Notes in Computer Science},
	pages = {128--143},
	title = {{A code generator framework for Isabelle/HOL}},
	volume = {4732},
	year = {2007}}

@book{milner1997definition,
	author = {Milner, Robin},
	publisher = {MIT press},
	title = {{The definition of standard ML: revised}},
	year = {1997}}

@article{thiebaux2005defense,
	author = {Thi{\'e}baux, Sylvie and Hoffmann, J{\"o}rg and Nebel, Bernhard},
	journal = {Artificial Intelligence},
	number = {1-2},
	pages = {38--69},
	publisher = {Elsevier},
	title = {{In defense of PDDL axioms}},
	volume = {168},
	year = {2005}}

@article{eriksson2017unsolvability,
	author = {Eriksson, Salom{\'e} and R{\"o}ger, Gabriele and Helmert, Malte},
	title = {Unsolvability Certificates for Classical Planning},
	year = {2017}}

@article{backstrom1995complexity,
	author = {B{\"a}ckstr{\"o}m, Christer and Nebel, Bernhard},
	journal = {Computational Intelligence},
	number = {4},
	pages = {625--655},
	publisher = {Wiley Online Library},
	title = {Complexity results for SAS+ planning},
	volume = {11},
	year = {1995}}

@article{jonsson1998state,
	author = {Jonsson, Peter and B{\"a}ckstr{\"o}m, Christer},
	journal = {Artificial Intelligence},
	number = {1-2},
	pages = {125--176},
	publisher = {Elsevier},
	title = {State-variable planning under structural restrictions: Algorithms and complexity},
	volume = {100},
	year = {1998}}

@inproceedings{kumar2014hol,
	author = {Kumar, Ramana and Arthan, Rob and Myreen, Magnus O and Owens, Scott},
	booktitle = {ITP},
	title = {{HOL with definitions: Semantics, soundness, and a verified implementation}},
	year = {2014}}

@inproceedings{kumar2014holL,
	author = {Kumar, Ramana and Arthan, Rob and Myreen, Magnus O and Owens, Scott},
	booktitle = {International Conference on Interactive Theorem Proving},
	organization = {Springer},
	pages = {308--324},
	title = {HOL with definitions: Semantics, soundness, and a verified implementation},
	year = {2014}}

@inproceedings{blanchette2016verified,
	author = {Blanchette, Jasmin Christian and Fleury, Mathias and Weidenbach, Christoph},
	booktitle = {International Joint Conference on Automated Reasoning},
	organization = {Springer},
	pages = {25--44},
	title = {{A verified SAT solver framework with learn, forget, restart, and incrementality}},
	year = {2016}}

@inproceedings{balyo2013relaxingL,
	author = {Balyo, Toma},
	booktitle = {Tools with Artificial Intelligence (ICTAI), 2013 IEEE 25th International Conference on},
	organization = {IEEE},
	pages = {865--871},
	title = {Relaxing the relaxed exist-step parallel planning semantics},
	year = {2013}}

@inproceedings{balyo2013relaxing,
	author = {Balyo, Toma},
	booktitle = {Tools with Artificial Intelligence (ICTAI), 2013},
	organization = {IEEE},
	pages = {865--871},
	title = {Relaxing the relaxed exist-step parallel planning semantics},
	year = {2013}}

@inproceedings{DBLP:conf/sat/Lammich17,
	author = {Peter Lammich},
	bibsource = {dblp computer science bibliography, http://dblp.org},
	biburl = {http://dblp.uni-trier.de/rec/bib/conf/sat/Lammich17},
	booktitle = {Theory and Applications of Satisfiability Testing - {SAT} 2017 - 20th International Conference, Melbourne, VIC, Australia, August 28 - September 1, 2017, Proceedings},
	crossref = {DBLP:conf/sat/2017},
	doi = {10.1007/978-3-319-66263-3_29},
	timestamp = {Tue, 15 Aug 2017 09:56:48 +0200},
	title = {The {GRAT} Tool Chain - Efficient {(UN)SAT} Certificate Checking with Formal Correctness Guarantees},
	url = {https://doi.org/10.1007/978-3-319-66263-3_29},
	year = {2017},
	Bdsk-Url-1 = {https://doi.org/10.1007/978-3-319-66263-3_29}}

@inproceedings{DBLP:conf/cade/Lammich17,
	author = {Peter Lammich},
	bibsource = {dblp computer science bibliography, http://dblp.org},
	biburl = {http://dblp.uni-trier.de/rec/bib/conf/cade/Lammich17},
	booktitle = {{CADE}},
	doi = {10.1007/978-3-319-63046-5_15},
	timestamp = {Wed, 12 Jul 2017 10:22:36 +0200},
	title = {Efficient Verified {(UN)SAT} Certificate Checking},
	url = {https://doi.org/10.1007/978-3-319-63046-5_15},
	year = {2017},
	Bdsk-Url-1 = {https://doi.org/10.1007/978-3-319-63046-5_15}}

@inproceedings{DBLP:conf/cade/Lammich17L,
	author = {Peter Lammich},
	bibsource = {dblp computer science bibliography, http://dblp.org},
	biburl = {http://dblp.uni-trier.de/rec/bib/conf/cade/Lammich17},
	booktitle = {Automated Deduction - {CADE} 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings},
	doi = {10.1007/978-3-319-63046-5_15},
	pages = {237--254},
	timestamp = {Wed, 12 Jul 2017 10:22:36 +0200},
	title = {Efficient Verified {(UN)SAT} Certificate Checking},
	url = {https://doi.org/10.1007/978-3-319-63046-5_15},
	year = {2017},
	Bdsk-Url-1 = {https://doi.org/10.1007/978-3-319-63046-5_15}}

@inproceedings{lochbihler2013light,
	author = {Lochbihler, Andreas},
	booktitle = {International Conference on Interactive Theorem Proving},
	organization = {Springer},
	pages = {116--132},
	title = {{Light-weight containers for Isabelle: efficient, extensible, nestable}},
	year = {2013}}

@article{kovacscomplete,
	author = {Kovacs, Daniel L},
	journal = {IPC-2011},
	title = {{BNF definition of PDDL 3.1}},
	year = {2011}}

@techreport{milner1972logic,
	author = {Milner, Robin},
	institution = {Stanford University},
	title = {Logic for computable functions description of a machine implementation},
	year = {1972}}

@techreport{green1969application,
	author = {Green, Cordell},
	institution = {SRI},
	title = {Application of theorem proving to problem solving},
	year = {1969}}

@inproceedings{lifschitz1987semantics,
	author = {Lifschitz, Vladimir},
	booktitle = {Reasoning about Actions and Plans: Proceedings of the 1986 Workshop},
	pages = {1--9},
	title = {On the semantics of STRIPS},
	year = {1987}}

@article{pednault1989adl,
	author = {Pednault, Edwin PD},
	journal = {Kr},
	pages = {324--332},
	title = {ADL: Exploring the Middle Ground Between STRIPS and the Situation Calculus.},
	volume = {89},
	year = {1989}}

@inproceedings{paulson2010three,
	author = {Paulson, Lawrence C and Blanchette, Jasmin Christian},
	booktitle = {PAAR@ IJCAR},
	pages = {1--10},
	title = {Three Years of Experience with Sledgehammer, a Practical Link between Automatic and Interactive Theorem Provers.},
	year = {2010}}

@inproceedings{zhan2016auto2,
	author = {Zhan, Bohua},
	booktitle = {International Conference on Interactive Theorem Proving},
	organization = {Springer},
	pages = {441--456},
	title = {AUTO2, a saturation-based heuristic prover for higher-order logic},
	year = {2016}}

@article{DBLP:journals/afp/MichaelisN17,
	author = {Julius Michaelis and Tobias Nipkow},
	bibsource = {dblp computer science bibliography, http://dblp.org},
	biburl = {http://dblp.org/rec/bib/journals/afp/MichaelisN17},
	journal = {Archive of Formal Proofs},
	timestamp = {Fri, 30 Jun 2017 19:26:27 +0200},
	title = {Propositional Proof Systems},
	url = {https://www.isa-afp.org/entries/Propositional_Proof_Systems.shtml},
	volume = {2017},
	year = {2017},
	Bdsk-Url-1 = {https://www.isa-afp.org/entries/Propositional_Proof_Systems.shtml}}

@inproceedings{MichaelisN-TYPES17,
	author = {Julius Michaelis and Tobias Nipkow},
	booktitle = {23rd Int.\ Conf.\ Types for Proofs and Programs (TYPES 2017)},
	editor = {A. Abel and F. Nordvall Forsberg and A. Kaposi},
	pages = {6:1--6:16},
	publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
	series = {LIPIcs},
	title = {Formalized Proof Systems for Propositional Logic},
	volume = {104},
	year = {2018}}

@inproceedings{haslum2003domain,
	author = {Haslum, Patrik and Scholz, Ulrich},
	booktitle = {ICAPS Workshop on PDDL},
	title = {Domain knowledge in planning: Representation and use},
	year = {2003}}

@article{haslum2011computing,
	author = {Haslum, Patrik and et al.},
	publisher = {AAAI Press},
	title = {Computing genome edit distances using domain-independent planning},
	year = {2011}}

@techreport{mccarthy1985formalization,
	author = {McCarthy, John},
	institution = {Citeseer},
	title = {{Formalization of STRIPS in situation calculus}},
	year = {1985}}

@techreport{norrish1998c,
	author = {Norrish, Michael},
	institution = {University of Cambridge, Computer Laboratory},
	title = {{C formalised in HOL}},
	year = {1998}}

@inproceedings{ictai2018,
	author = {Abdulaziz, Mohammad and Lammich, Peter},
	booktitle = {International Conference on Tools in Artificial Intelligence (ICTAI)},
	organization = {IEEE},
	title = {{A Formally Verified Validator for Classical Planning Problems and Solutions}},
	year = {2018}}

@article{Propositional_Proof_Systems-AFP,
	author = {Julius Michaelis and Tobias Nipkow},
	issn = {2150-914x},
	journal = {Archive of Formal Proofs},
	month = jun,
	note = {\url{http://isa-afp.org/entries/Propositional_Proof_Systems.html}, Formal proof development},
	title = {Propositional Proof Systems},
	year = 2017}

@article{DBLP:journals/ai/RintanenHN06,
	author = {Jussi Rintanen and Keijo Heljanko and Ilkka Niemel{\"{a}}},
	bibsource = {dblp computer science bibliography, https://dblp.org},
	biburl = {https://dblp.org/rec/journals/ai/RintanenHN06.bib},
	doi = {10.1016/j.artint.2006.08.002},
	journal = {Artif. Intell.},
	number = {12-13},
	pages = {1031--1080},
	timestamp = {Mon, 05 Jun 2017 12:38:26 +0200},
	title = {Planning as satisfiability: parallel plans and algorithms for plan search},
	url = {https://doi.org/10.1016/j.artint.2006.08.002},
	volume = {170},
	year = {2006},
	Bdsk-Url-1 = {https://doi.org/10.1016/j.artint.2006.08.002}}

@misc{abdulaziz2020formally,
	archiveprefix = {arXiv},
	author = {Mohammad Abdulaziz and Friedrich Kurz},
	eprint = {2010.14648},
	primaryclass = {cs.AI},
	title = {Formally Verified SAT-Based AI Planning},
	year = {2020}}

@manual{wenzel--2018,
  author = {Makarius Wenzel},
  title = {The {Isabelle/Isar} Reference Manual},
  year = 2018,
  note = {\url{https://isabelle.in.tum.de/doc/isar-ref.pdf}}}
