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

@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},
  title     = {Symbolic Model Checking without {BDDs}},
  booktitle = {{TACAS}},
  pages     = {193--207},
  year      = {1999}
}

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


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

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

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



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

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

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

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

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

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

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

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


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

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

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


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



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


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

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

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

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


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


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

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

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



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

@article{hart:etal:68,
  author    = {P. E. Hart and
               N. J. Nilsson and
               B. Raphael},
  title     = {A Formal Basis for the Heuristic Determination of Minimum
               Cost Paths},
  journal   = {IEEE Trans. Systems Science and Cybernetics},
  volume    = {4},
  number    = {2},
  year      = {1968},
  pages     = {100--107},
  ee        = {http://dx.doi.org/10.1109/TSSC.1968.300136},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{haslum:geffner:00,
  author    = {P. Haslum and
               H. Geffner},
  title     = {Admissible Heuristics for Optimal Planning},
  booktitle = {Proc. Int. Conf. on AI Planning Systems},
  year      = {2000},
  pages     = {140--149},
  ee        = {http://www.aaai.org/Library/AIPS/2000/aips00-015.php},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

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

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



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


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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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


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

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

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


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

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


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

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

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

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

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

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

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

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


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

@inproceedings{bundala2012magnitude,
  title        = {On the magnitude of completeness thresholds in bounded model checking},
  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},
  pages        = {155--164},
  year         = {2012},
  organization = {IEEE Computer Society}
}

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

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

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

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

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

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

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

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

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

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

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

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

@inproceedings{chechik2014better,
  title        = {Better approximation algorithms for the graph diameter},
  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},
  pages        = {1041--1052},
  year         = {2014},
  organization = {Society for Industrial and Applied Mathematics}
}

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

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

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

@article{bulterman2002computing,
  title     = {On computing a longest path in a tree},
  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},
  volume    = {81},
  number    = {2},
  pages     = {93--96},
  year      = {2002},
  publisher = {Elsevier North-Holland, Inc.}
}

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

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

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

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

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

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

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

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

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



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


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



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


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


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

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

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


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

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

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


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

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


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

@inproceedings{JoslinR97,
  author    = {David Joslin and
               Amitabha Roy},
  title     = {Exploiting Symmetry in Lifted {CSPs}},
  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},
  year      = {1997},
  timestamp = {Tue, 11 Dec 2012 12:57:22 +0100},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/aaai/JoslinR97},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

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


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

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


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

@inproceedings{FoxL99,
  author    = {Maria Fox and
               Derek Long},
  title     = {The Detection and Exploitation of Symmetry in Planning Problems},
  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},
  year      = {1999},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/ijcai/FoxL99},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

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

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

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

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

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


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


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

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

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

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

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

@article{dufourd2009intuitionistic,
  title     = {{An intuitionistic proof of a discrete form of the Jordan Curve Theorem formalized in Coq with combinatorial hypermaps}},
  author    = {Dufourd, Jean-Fran{\c{c}}ois},
  journal   = {Journal of Automated Reasoning},
  volume    = {43},
  number    = {1},
  pages     = {19--51},
  year      = {2009},
  publisher = {Springer}
}
@article{bezem2008mechanization,
  title     = {{On the mechanization of the proof of Hessenberg's theorem in coherent logic}},
  author    = {Bezem, Marc and Hendriks, Dimitri},
  journal   = {Journal of Automated Reasoning},
  volume    = {40},
  number    = {1},
  pages     = {61--85},
  year      = {2008},
  publisher = {Springer}
}
@article{mckinna1999some,
  title     = {Some lambda calculus and type theory formalized},
  author    = {McKinna, James and Pollack, Robert},
  journal   = {Journal of Automated Reasoning},
  volume    = {23},
  number    = {3},
  pages     = {373--409},
  year      = {1999},
  publisher = {Springer}
}

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

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

@article{kamareddine2003formalizing,
  title     = {Formalizing strong normalization proofs of explicit substitution calculi in ALF},
  author    = {Kamareddine, Fairouz and Qiao, Haiyan},
  journal   = {Journal of Automated Reasoning},
  volume    = {30},
  number    = {1},
  pages     = {59--98},
  year      = {2003},
  publisher = {Springer}
}
@article{manolios2005ordinal,
  title     = {Ordinal arithmetic: Algorithms and mechanization},
  author    = {Manolios, Panagiotis and Vroon, Daron},
  journal   = {Journal of Automated Reasoning},
  volume    = {34},
  number    = {4},
  pages     = {387--423},
  year      = {2005},
  publisher = {Springer}
}
@article{maric2009formalization,
  title     = {{Formalization and implementation of modern SAT solvers}},
  author    = {Mari{\'c}, Filip},
  journal   = {Journal of Automated Reasoning},
  volume    = {43},
  number    = {1},
  year      = {2009},
  publisher = {Springer}
}


@inproceedings{klein2009sel4L,
  title        = {{seL4: Formal verification of an OS kernel}},
  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},
  pages        = {207--220},
  year         = {2009},
  organization = {ACM}
}

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

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

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

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

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

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

@incollection{hales2011revision,
  title     = {{A revision of the proof of the Kepler conjecture}},
  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},
  year      = {2011},
  publisher = {Springer}
}

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

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

@inproceedings{esparza2013fully,
  title        = {{A fully verified executable LTL model checker}},
  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},
  pages        = {463--478},
  year         = {2013},
  organization = {Springer}
}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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


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


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

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

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


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

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

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

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

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

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

@book{milner1997definition,
  title     = {{The definition of standard ML: revised}},
  author    = {Milner, Robin},
  year      = {1997},
  publisher = {MIT press}
}
@article{thiebaux2005defense,
  title     = {{In defense of PDDL axioms}},
  author    = {Thi{\'e}baux, Sylvie and Hoffmann, J{\"o}rg and Nebel, Bernhard},
  journal   = {Artificial Intelligence},
  volume    = {168},
  number    = {1-2},
  pages     = {38--69},
  year      = {2005},
  publisher = {Elsevier}
}

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

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

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

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

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


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

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

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

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


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

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


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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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