@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 = {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},
  journal={International Planning Competition},  
  year={2014}
}

@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{klein2009sel4,
  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}
}

@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{abdulaziz2018formally,
  title={Formally Verified Algorithms for Upper-Bounding State Space Diameters},
  author={Abdulaziz, Mohammad and Norrish, Michael and Gretton, Charles},
  journal={Journal of Automated Reasoning},
  pages={1--36},
  year={2018},
  publisher={Springer}
}

@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. 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={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}
}

@inproceedings{eriksson2017unsolvability,
  author    = {Salom{\'{e}} Eriksson and Gabriele R{\"{o}}ger and Malte Helmert},
  editor    = {Laura Barbulescu and
               Jeremy Frank and
               Mausam and
               Stephen F. Smith},
  title     = {Unsolvability Certificates for Classical Planning},
  booktitle = {Proceedings of the Twenty-Seventh International Conference on Automated
               Planning and Scheduling, {ICAPS} 2017, Pittsburgh, Pennsylvania, USA,
               June 18-23, 2017.},
  pages     = {88--97},
  publisher = {{AAAI} Press},
  year      = {2017},
  url       = {https://aaai.org/ocs/index.php/ICAPS/ICAPS17/paper/view/15734},
  timestamp = {Tue, 26 Sep 2017 07:41:36 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/aips/ErikssonRH17},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@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={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{balyo2013relaxing,
  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{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},
  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 = {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={Unpublished manuscript from the IPC-2011 website},
  year={2011}
}

@techreport{milner1972logic,
  title={Logic for computable functions description of a machine implementation},
  author={Milner, Robin},
  year={1972},
  institution={STANFORD UNIV CA DEPT OF COMPUTER SCIENCE}
}

@article{emerson1996symmetry,
  title={Symmetry and model checking},
  author={Emerson, E Allen and Sistla, A Prasad},
  journal={Formal methods in system design},
  volume={9},
  number={1},
  pages={105--131},
  year={1996},
  publisher={Springer}
}

@article{clarke1996exploiting,
  title={Exploiting symmetry in temporal logic model checking},
  author={Clarke, Edmund M and Enders, Reinhard and Filkorn, Thomas and Jha, Somesh},
  journal={Formal methods in system design},
  volume={9},
  number={1-2},
  pages={77--104},
  year={1996},
  publisher={Springer}
}

@inproceedings{alur1997partial,
  title={Partial-order reduction in symbolic state space exploration},
  author={Alur, Rajeev and Brayton, Robert K and Henzinger, Thomas A and Qadeer, Shaz and Rajamani, Sriram K},
  booktitle={International Conference on Computer Aided Verification},
  pages={340--351},
  year={1997},
  organization={Springer}
}

@inproceedings{gerth1995partial,
  title={A partial order approach to branching time logic model checking},
  author={Gerth, Rob and Kuiper, Ruurd and Peled, Doron and Penczek, Wojciech},
  booktitle={Theory of Computing and Systems, 1995. Proceedings., Third Israel Symposium on the},
  pages={130--139},
  year={1995},
  organization={IEEE}
}

@inproceedings{godefroid1990using,
  title={Using partial orders to improve automatic verification methods},
  author={Godefroid, Patrice},
  booktitle={International Conference on Computer Aided Verification},
  pages={176--185},
  year={1990},
  organization={Springer}
}

@inproceedings{chen2009completeness,
  title={Completeness and Optimality Preserving Reduction for Planning.},
  author={Chen, Yixin and Yao, Guohui},
  booktitle={IJCAI},
  pages={1659--1664},
  year={2009}
}

@article{xu2011theory,
  title={Theory and algorithms for partial order based reduction in planning},
  author={Xu, You and Chen, Yixin and Lu, Qiang and Huang, Ruoyun},
  journal={arXiv preprint arXiv:1106.5427},
  year={2011}
}

@article{blum1997fast,
  title={Fast planning through planning graph analysis},
  author={Blum, Avrim L and Furst, Merrick L},
  journal={Artificial intelligence},
  volume={90},
  number={1},
  pages={281--300},
  year={1997},
  publisher={Elsevier}
}

@inproceedings{mcdermott1996heuristic,
  title={A Heuristic Estimator for Means-Ends Analysis in Planning.},
  author={McDermott, Drew V},
  booktitle={AIPS},
  volume={96},
  pages={142--149},
  year={1996}
}

@article{pnueli2002small,
  title={The small model property: How small can it be?},
  author={Pnueli, Amir and Rodeh, Yoav and Strichman, Ofer and Siegel, Michael},
  journal={Information and computation},
  volume={178},
  number={1},
  pages={279--293},
  year={2002},
  publisher={Elsevier}
}

@article{hoffmann2001ff,
  title={The FF planning system: Fast plan generation through heuristic search},
  author={Hoffmann, J{\"o}rg and Nebel, Bernhard},
  journal={Journal of Artificial Intelligence Research},
  volume={14},
  pages={253--302},
  year={2001}
}

@incollection{mccarthy1981some,
  title={Some philosophical problems from the standpoint of artificial intelligence},
  author={McCarthy, John and Hayes, Patrick J},
  booktitle={Readings in artificial intelligence},
  pages={431--450},
  year={1981},
  publisher={Elsevier}
}

@incollection{lifschitz1987semantics,
  title={On the semantics of STRIPS},
  author={Lifschitz, Vladimir},
  booktitle={Reasoning About Actions \& Plans},
  pages={1--9},
  year={1987},
  publisher={Elsevier}
}