@STRING{cav	= {CAV} }
@STRING{flops	= {FLOPS} }
@STRING{fsttcs	= {FSTTCS} }
@STRING{itp	= {ITP} }
@STRING{lncs	= {LNCS} }
@STRING{lncs	= {LNCS} }
@STRING{springer= {Springer} }
@STRING{springer= {Springer} }
@STRING{tacas	= {TACAS} }
@STRING{tphols	= {TPHOLs} }

@InProceedings{La14_ITP,
  author  = {Peter Lammich},
  booktitle = {Proc. of ITP},
  title   = {Verified Efficient Implementation of {Gabow's} Strongly Connected Component Algorithm},
  year    = 2014,
  note = "to appear"
}

@article{Loch13_words,
  author  = {Andreas Lochbihler},
  title   = {Native Word},
  journal = {Archive of Formal Proofs},
  month   = sep,
  year    = 2013,
  note    = {\url{http://isa-afp.org/entries/Native_Word.shtml},
            Formal proof development},
  ISSN    = {2150-914x},
}

@Book{MTHM97,
 author = {Robin Milner and Mads Tofte and Robert Harper and D. MacQueen},
 title = "The Definition of Standard ML (Revised)",
 publisher = "MIT Press",
 year = "1997",
 isbn = "0262631814"
}

@misc{La14_Gabow_Thys,
  author = "Peter Lammich",
  title = "Formalization of Gabow's Algorithm",
  note = "Isabelle Theories",
  url="http://www21.in.tum.de/~lammich/isabelle/gabow"
}

@misc{PolyML,
  author = "Matthews, David",
  title = "{P}oly/{ML}",
  url="http://www.polyml.org"
}

@Book{		  abrial96,
  author	= "Jean-Raymond Abrial",
  title		= "The B-Book: Assigning Programs to Meanings",
  publisher	= "Cambridge University Press",
  year		= 1996
}

###Book{	  abrial96,
  author	= "Jean-Raymond Abrial",
  title		= "The B-Book: Assigning Programs to Meanings",
  publisher	= "Cambridge University Press",
  year		= 1996
}

@Article{	  amr07,
  author	= {Almeida, Marco and Moreira, Nelma and Reis, Rog\'{e}rio},
  title		= {Enumeration and generation with a string automata
		  representation},
  journal	= {Theor. Comput. Sci.},
  volume	= {387},
  issue		= {2},
  month		= {November},
  year		= {2007},
  issn		= {0304-3975},
  pages		= {93--102},
  numpages	= {10},
  url		= {http://dl.acm.org/citation.cfm?id=1297415.1297473},
  acmid		= {1297473},
  publisher	= {Elsevier Science Publishers Ltd.},
  address	= {Essex, UK},
  keywords	= {Exact enumeration, Finite automata, Initially-connected
		  deterministic finite automata, Minimal automata, Random
		  generation}
}

###Article{	  amr07,
  author	= {Almeida, Marco and Moreira, Nelma and Reis, Rog\'{e}rio},
  title		= {Enumeration and generation with a string automata
		  representation},
  journal	= {Theor. Comput. Sci.},
  volume	= {387},
  issue		= {2},
  month		= {November},
  year		= {2007},
  issn		= {0304-3975},
  pages		= {93--102},
  numpages	= {10},
  url		= {http://dl.acm.org/citation.cfm?id=1297415.1297473},
  doi		= {10.1016/j.tcs.2007.07.029},
  acmid		= {1297473},
  publisher	= {Elsevier Science Publishers Ltd.},
  address	= {Essex, UK},
  keywords	= {Exact enumeration, Finite automata, Initially-connected
		  deterministic finite automata, Minimal automata, Random
		  generation}
}

@InProceedings{	  bac06,
  author	= {Baclet, Manuel and Pagetti, Claire},
  booktitle	= {Proc. of CIAA 2006},
  journal	= {Implementation and Application of Automata},
  pages		= {114--125},
  title		= {Around {H}opcroft's Algorithm},
  volume	= {LNCS 4094},
  year		= 2006
}

###InProceedings{ bac06,
  author	= {Baclet, Manuel and Pagetti, Claire},
  booktitle	= {Proc. of CIAA 2006},
  journal	= {Implementation and Application of Automata},
  pages		= {114--125},
  title		= {{Around Hopcroft's Algorithm}},
  volume	= {LNCS 4094},
  year		= 2006
}

@PhDThesis{	  back78,
  author	= {Ralph-Johan Back},
  title		= {On the correctness of refinement steps in program
		  development},
  school	= {Department of Computer Science, University of Helsinki},
  year		= {1978}
}

###PhDThesis{	  back78,
  author	= {Ralph-Johan Back},
  title		= {On the correctness of refinement steps in program
		  development},
  school	= {Department of Computer Science, University of Helsinki},
  year		= {1978}
}

@Book{		  baierkatoen:2008:modelchecking,
  title		= {Principles of Model Checking},
  publisher	= {MIT Press},
  year		= {2008},
  author	= {Christel Baier and Joost-Pieter Katoen}
}

###Book{	  baierkatoen:2008:modelchecking,
  title		= {Principles of Model Checking},
  publisher	= {MIT Press},
  year		= {2008},
  author	= {Christel Baier and Joost-Pieter Katoen}
}

@InProceedings{	  ballarin:2006:mkm,
  author	= "Clemens Ballarin",
  title		= "Interpretation of Locales in {Isabelle}: Theories and
		  Proof Contexts",
  editor	= "J. M. Borwein and W. M. Farmer",
  booktitle	= "MKM 2006",
  series	= "LNAI",
  volume	= "4108",
  pages		= "31--43",
  year		= 2006,
  publisher	= springer
}

###InProceedings{ ballarin:2006:mkm,
  author	= "Clemens Ballarin",
  title		= "Interpretation of Locales in {Isabelle}: Theories and
		  Proof Contexts",
  editor	= "J. M. Borwein and W. M. Farmer",
  booktitle	= "MKM 2006",
  series	= "LNAI",
  volume	= "4108",
  pages		= "31--43",
  year		= 2006,
  publisher	= springer
}

@Article{	  bawr00,
  title		= {Encoding, Decoding and Data Refinement},
  author	= {Back, Ralph-Johan and von Wright, Joakim},
  journal	= {Formal Aspects of Computing},
  volume	= {12},
  pages		= {313--349},
  year		= {2000}
}

###Article{	  bawr00,
  title		= {Encoding, Decoding and Data Refinement},
  author	= {Back, Ralph-Johan and von Wright, Joakim},
  journal	= {Formal Aspects of Computing},
  volume	= {12},
  pages		= {313--349},
  year		= {2000}
}

@Article{	  bawr90,
  author	= {R. J. R. Back and J. von Wright},
  title		= {Refinement Concepts Formalized in Higher Order Logic},
  journal	= {Formal Aspects of Computing},
  year		= {1990},
  volume	= {2}
}

###Article{	  bawr90,
  author	= {R. J. R. Back and J. von Wright},
  title		= {Refinement Concepts Formalized in Higher Order Logic},
  journal	= {Formal Aspects of Computing},
  year		= {1990},
  volume	= {2}
}

@Book{		  bawr98,
  author	= {Ralph-Johan Back and Joakim von Wright},
  title		= {Refinement Calculus --- A Systematic Introduction},
  publisher	= springer,
  year		= {1998}
}

###Book{	  bawr98,
  author	= {Ralph-Johan Back and Joakim von Wright},
  title		= {Refinement Calculus --- A Systematic Introduction},
  publisher	= springer,
  year		= {1998}
}

@InProceedings{	  bbmv91,
  author	= {Roland C. Backhouse and Peter de Bruin and Grant Malcolm
		  and Ed Voermans and Jaap van der Woude},
  title		= {Relational catamorphisms},
  booktitle	= {Proc. of the IFIP TC2/WG2.1 Working Conference on
		  Constructing Programs},
  publisher	= {Elsevier Science Publishers BV},
  year		= {1991}
}

@InProceedings{	  bere09,
  author	= {Berghofer, Stefan and Reiter, Markus},
  title		= {Formalizing the Logic-Automaton Connection},
  booktitle	= {TPHOLs '09},
  year		= {2009},
  isbn		= {978-3-642-03358-2},
  pages		= {147--163},
  location	= {Munich, Germany},
  publisher	= springer,
  address	= {Berlin, Heidelberg}
}

###InProceedings{ bere09,
  author	= {Berghofer, Stefan and Reiter, Markus},
  title		= {Formalizing the Logic-Automaton Connection},
  booktitle	= {TPHOLs '09},
  year		= {2009},
  isbn		= {978-3-642-03358-2},
  pages		= {147--163},
  location	= {Munich, Germany},
  doi		= {https://doi.org/10.1007/978-3-642-03359-9_12},
  publisher	= springer,
  address	= {Berlin, Heidelberg}
}

@InCollection{	  bere09_afp,
  author	= {Stefan Berghofer and Markus Reiter},
  title		= {Formalizing the Logic-Automaton Connection },
  booktitle	= {Archive of Formal Proofs},
  editor	= {Gerwin Klein and Tobias Nipkow and Lawrence Paulson},
  publisher	= {\url{http://isa-afp.org/entries/Presburger-Automata.shtml}}
		  ,
  month		= dec,
  year		= 2009,
  note		= {Formal proof development},
  issn		= {2150-914x}
}

###InCollection{  bere09_afp,
  author	= {Stefan Berghofer and Markus Reiter},
  title		= {Formalizing the Logic-Automaton Connection },
  booktitle	= {Archive of Formal Proofs},
  editor	= {Gerwin Klein and Tobias Nipkow and Lawrence Paulson},
  publisher	= {\url{http://isa-afp.org/entries/Presburger-Automata.shtml}}
		  ,
  month		= dec,
  year		= 2009,
  note		= {Formal proof development},
  issn		= {2150-914x}
}

@InCollection{	  bjjm99,
  year		= {1999},
  booktitle	= {Advanced Functional Programming},
  volume	= {1608},
  series	= lncs,
  title		= {Generic Programming},
  publisher	= springer,
  author	= {Backhouse, Roland and Jansson, Patrik and Jeuring, Johan
		  and Meertens, Lambert},
  pages		= {28-115}
}

@InProceedings{	  bkhem08,
  author	= {Bulwahn, Lukas and Krauss, Alexander and Haftmann, Florian
		  and Erk\"{o}k, Levent and Matthews, John},
  title		= {Imperative Functional Programming with {Isabelle/HOL}},
  booktitle	= {TPHOLs '08},
  year		= {2008},
  isbn		= {978-3-540-71065-3},
  location	= {Montreal, P.Q., Canada},
  pages		= {134--149},
  numpages	= {16},
  url		= {http://portal.acm.org/citation.cfm?id=1459784.1459801},
  acmid		= {1459801},
  publisher	= springer,
  series	= lncs,
  volume	= {5170},
  address	= {Berlin, Heidelberg}
}

###InProceedings{ bkhem08,
  author	= {Bulwahn, Lukas and Krauss, Alexander and Haftmann, Florian
		  and Erk\"{o}k, Levent and Matthews, John},
  title		= {Imperative Functional Programming with {Isabelle/HOL}},
  booktitle	= {TPHOLs '08},
  year		= {2008},
  isbn		= {978-3-540-71065-3},
  location	= {Montreal, P.Q., Canada},
  pages		= {134--149},
  numpages	= {16},
  url		= {http://portal.acm.org/citation.cfm?id=1459784.1459801},
  doi		= {10.1007/978-3-540-71067-7_14},
  acmid		= {1459801},
  publisher	= springer,
  series	= lncs,
  volume	= {5170},
  address	= {Berlin, Heidelberg}
}

@Article{	  blum96,
  title		= {An {O}(n log n) implementation of the standard method for
		  minimizing n-state finite automata},
  volume	= {6},
  number	= {2},
  journal	= {Information Processing Letters},
  author	= {Blum, Norbert},
  year		= {1996},
  pages		= {65--69}
}

###Article{	  blum96,
  title		= {An {O}(n log n) implementation of the standard method for
		  minimizing n-state finite automata},
  volume	= {6},
  number	= {2},
  journal	= {Information Processing Letters},
  author	= {Blum, Norbert},
  year		= {1996},
  pages		= {65--69}
}

@InProceedings{	  bra09,
  author	= {Thomas Braibant and Damien Pous},
  title		= {A tactic for deciding {K}leene algebras},
  booktitle	= {First Coq Workshop},
  year		= {2009}
}

###InProceedings{ bra09,
  author	= {Thomas Braibant and Damien Pous},
  title		= {A tactic for deciding Kleene algebras},
  booktitle	= {First Coq Workshop},
  year		= {2009}
}

@InCollection{	  brz62,
  author	= {J. A. Brzozowski},
  title		= {Canonical regular expressions and minimal state graphs for
		  definite events},
  booktitle	= {Mathematical theory of Automata},
  note		= {Volume 12 of MRI Symposia Series},
  pages		= {529--561},
  publisher	= {Polytechnic Press, Polytechnic Institute of Brooklyn,
		  N.Y.},
  year		= {1962}
}

###InCollection{  brz62,
  author	= {J. A. Brzozowski},
  title		= {Canonical regular expressions and minimal state graphs for
		  definite events},
  booktitle	= {Mathematical theory of Automata},
  note		= {Volume 12 of MRI Symposia Series},
  pages		= {529--561},
  publisher	= {Polytechnic Press, Polytechnic Institute of Brooklyn,
		  N.Y.},
  year		= {1962}
}

@InProceedings{	  bu62,
  author	= {Buechi, Julius R.},
  booktitle	= {International Congress on Logic, Methodology, and
		  Philosophy of Science},
  citeulike-article-id={2948751},
  keywords	= {automata\_theory},
  pages		= {1--11},
  posted-at	= {2008-07-01 16:58:48},
  priority	= {0},
  publisher	= {Stanford University Press},
  title		= {{On a Decision Method in Restricted Second-Order
		  Arithmetic}},
  year		= {1962}
}

@InProceedings{	  bul12,
  author	= {Lukas Bulwahn},
  title		= {The New Quickcheck in {I}sabelle: Random, Exhaustive and
		  Symbolic Testing Under One Roof},
  booktitle	= {Proc. of CPP},
  year		= {2012},
  publisher	= springer,
  volume	= {7679},
  pages		= {92--108},
  series	= lncs
}

@TechReport{	  c++stl,
  author	= {Alexander Stepanov and Meng Lee},
  title		= {The Standard Template Library},
  institution	= {HP Laboratories},
  year		= {1995},
  month		= {November},
  number	= {95-11(R.1)}
}

###TechReport{	  c++stl,
  author	= {Alexander Stepanov and Meng Lee},
  title		= {The Standard Template Library},
  institution	= {HP Laboratories},
  year		= {1995},
  month		= {November},
  number	= {95-11(R.1)}
}

@InProceedings{	  cdp05,
  author	= {Couvreur, Jean-Michel and Duret-Lutz, Alexandre and
		  Poitrenaud, Denis},
  title		= {On-the-fly Emptiness Checks for Generalized B{\"u}chi Automata},
  booktitle	= {Proc. of SPIN},
  year		= {2005},
  pages		= {169--184},
  numpages	= {16},
  publisher	= {Springer},
}

@Article{	  chme96,
  year		= {1996},
  journal	= {Algorithmica},
  volume	= {15},
  number	= {6},
  title		= {Algorithms for dense graphs and networks on the random
		  access computer},
  publisher	= {Springer-Verlag},
  author	= {Cheriyan, J. and Mehlhorn, K.},
  pages		= {521-549},
  language	= {English}
}

@Article{	  choysingh:1994:leaderfilters,
  author	= {Choy, Manhoi and Singh, Ambuj K.},
  title		= {Adaptive solutions to the mutual exclusion problem},
  journal	= {Distributed Computing},
  year		= {1994},
  volume	= {8},
  pages		= {1--17},
  number	= {1},
  issn		= {0178-2770},
  keywords	= {Adaptive algorithms; Leader election; Mutual exclusion;
		  Synchronization},
  language	= {English},
  publisher	= springer
}

###Article{	  choysingh:1994:leaderfilters,
  author	= {Choy, Manhoi and Singh, Ambuj K.},
  title		= {Adaptive solutions to the mutual exclusion problem},
  journal	= {Distributed Computing},
  year		= {1994},
  volume	= {8},
  pages		= {1--17},
  number	= {1},
  issn		= {0178-2770},
  keywords	= {Adaptive algorithms; Leader election; Mutual exclusion;
		  Synchronization},
  language	= {English},
  publisher	= springer
}

@InProceedings{	  cks08,
  author	= {David Cock and Gerwin Klein and Thomas Sewell},
  title		= {Secure Microkernels, State Monads and Scalable
		  Refinement},
  booktitle	= {Proc. of TPHOLs},
  year		= {2008},
  series	= lncs,
  publisher	= springer,
  pages		= {167--182},
  volume	= {5170}
}

###InProceedings{ cks08,
  author	= {David Cock and Gerwin Klein and Thomas Sewell},
  title		= {Secure Microkernels, State Monads and Scalable
		  Refinement},
  booktitle	= {Proc. of TPHOLs},
  year		= {2008},
  series	= lncs,
  publisher	= springer,
  pages		= {167--182},
  volume	= {5170}
}

@Misc{		  con97,
  author	= {Robert L. Constable and Paul B. Jackson and Pavel Naumov
		  and Juan Uribe},
  title		= {Formalizing Automata Theory {I}: Finite Automata},
  year		= {1997}
}

###Misc{	  con97,
  author	= {Robert L. Constable and Paul B. Jackson and Pavel Naumov
		  and Juan Uribe},
  title		= {Formalizing Automata Theory I: Finite Automata},
  year		= {1997}
}

@Misc{		  coq:std:lib,
  key		= "Coq",
  title		= "The {Coq} Standard Library",
  url		= "http://coq.inria.fr/stdlib/index.html"
}

###Misc{	  coq:std:lib,
  key		= "Coq",
  title		= "The {Coq} Standard Library",
  url		= "http://coq.inria.fr/stdlib/index.html"
}

@Article{	  CVWY92,
  author	= {Courcoubetis, C. and Vardi, M. and Wolper, P. and
		  Yannakakis, M.},
  title		= {Memory-efficient algorithms for the verification of
		  temporal properties},
  journal	= {Formal Methods in System Design},
  year		= {1992},
  volume	= {1},
  pages		= {275--288},
  number	= {2/3},
  abstract	= {This article addresses the problem of designing
		  memory-efficient algorithms for the verification of
		  temporal properties of finite-state programs. Both the
		  programs and their desired temporal properties are modeled
		  as automata on infinite words (B{\"u}chi automata).
		  Verification is then reduced to checking the emptiness of
		  the automaton resulting from the product of the program and
		  the property. This problem is usually solved by computing
		  the strongly connected components of the graph representing
		  the product automaton. Here, we present algorithms that
		  solve the emptiness problem without explicitly constructing
		  the strongly connected components of the product graph. By
		  allowing the algorithms to err with some probability, we
		  can implement them with a randomly accessed memory of size
		  O(n) bits, where n is the number of states of the graph,
		  instead of O(n log n) bits that the presently known
		  algorithms require.},
  issn		= {0925-9856},
  issue		= {2},
  publisher	= springer
}

###Article{	  courcoubetisvardietal:1992:nesteddfs,
  author	= {Courcoubetis, C. and Vardi, M. and Wolper, P. and
		  Yannakakis, M.},
  title		= {Memory-efficient algorithms for the verification of
		  temporal properties},
  journal	= {Formal Methods in System Design},
  year		= {1992},
  volume	= {1},
  pages		= {275--288},
  number	= {2/3},
  abstract	= {This article addresses the problem of designing
		  memory-efficient algorithms for the verification of
		  temporal properties of finite-state programs. Both the
		  programs and their desired temporal properties are modeled
		  as automata on infinite words (B{\"u}chi automata).
		  Verification is then reduced to checking the emptiness of
		  the automaton resulting from the product of the program and
		  the property. This problem is usually solved by computing
		  the strongly connected components of the graph representing
		  the product automaton. Here, we present algorithms that
		  solve the emptiness problem without explicitly constructing
		  the strongly connected components of the product graph. By
		  allowing the algorithms to err with some probability, we
		  can implement them with a randomly accessed memory of size
		  O(n) bits, where n is the number of states of the graph,
		  instead of O(n log n) bits that the presently known
		  algorithms require.},
  issn		= {0925-9856},
  issue		= {2},
  publisher	= springer
}

@Proceedings{	  dblp:conf/cav/2001,
  editor	= {G{\'e}rard Berry and Hubert Comon and Alain Finkel},
  title		= {Computer Aided Verification, 13th International
		  Conference, CAV 2001, Paris, France, July 18-22, 2001,
		  Proceedings},
  booktitle	= cav,
  publisher	= springer,
  series	= lncs,
  volume	= {2102},
  year		= {2001},
  isbn		= {3-540-42345-1},
  bibsource	= {DBLP, http://dblp.uni-trier.de}
}

@Proceedings{	  dblp:conf/fsttcs/2001,
  editor	= {Ramesh Hariharan and Madhavan Mukund and V. Vinay},
  title		= {FST TCS 2001: Foundations of Software Technology and
		  Theoretical Computer Science, 21st Conference, Bangalore,
		  India, December 13-15, 2001, Proceedings},
  booktitle	= fsttcs,
  publisher	= springer,
  series	= lncs,
  volume	= {2245},
  year		= {2001},
  isbn		= {3-540-43002-4},
  bibsource	= {DBLP, http://dblp.uni-trier.de}
}

@Proceedings{	  dblp:conf/tacas/1996,
  editor	= {Tiziana Margaria and Bernhard Steffen},
  title		= {Tools and Algorithms for Construction and Analysis of
		  Systems},
  booktitle	= {TACAS},
  publisher	= springer,
  series	= lncs,
  volume	= {1055},
  year		= {1996},
  isbn		= {3-540-61042-1},
  bibsource	= {DBLP, http://dblp.uni-trier.de}
}

###Proceedings{	  dblp:conf/tacas/1996,
  editor	= {Tiziana Margaria and Bernhard Steffen},
  title		= {Tools and Algorithms for Construction and Analysis of
		  Systems, Second International Workshop, TACAS '96, Passau,
		  Germany, March 27-29, 1996, Proceedings},
  booktitle	= {TACAS},
  publisher	= springer,
  series	= lncs,
  volume	= {1055},
  year		= {1996},
  isbn		= {3-540-61042-1},
  bibsource	= {DBLP, http://dblp.uni-trier.de}
}

@InProceedings{	  dblp:conf/tacas/choup96,
  author	= {Ching-Tsun Chou and Doron Peled},
  title		= {Formal Verification of a Partial-Order Reduction Technique
		  for Model Checking},
  booktitle	= {Tools and Algorithms for the Construction and Analysis of
		  Systems (TACAS)},
  year		= {1996},
  pages		= {241--257},
  crossref	= {DBLP:conf/tacas/1996},
  bibsource	= {DBLP, http://dblp.uni-trier.de}
}

###InProceedings{ dblp:conf/tacas/choup96,
  author	= {Ching-Tsun Chou and Doron Peled},
  title		= {Formal Verification of a Partial-Order Reduction Technique
		  for Model Checking},
  booktitle	= {Tools and Algorithms for the Construction and Analysis of
		  Systems (TACAS)},
  year		= {1996},
  pages		= {241--257},
  ee		= {https://doi.org/10.1007/3-540-61042-1_48},
  crossref	= {DBLP:conf/tacas/1996},
  bibsource	= {DBLP, http://dblp.uni-trier.de}
}

@Proceedings{	  dblp:conf/wia/2009,
  editor	= {Sebastian Maneth},
  title		= {Implementation and Application of Automata},
  booktitle	= {CIAA},
  publisher	= springer,
  series	= lncs,
  volume	= {5642},
  year		= {2009},
  isbn		= {978-3-642-02978-3},
  ee		= {https://doi.org/10.1007/978-3-642-02979-0},
  bibsource	= {DBLP, http://dblp.uni-trier.de}
}

###Proceedings{	  dblp:conf/wia/2009,
  editor	= {Sebastian Maneth},
  title		= {Implementation and Application of Automata, 14th
		  International Conference, CIAA 2009, Sydney, Australia,
		  July 14-17, 2009. Proceedings},
  booktitle	= {CIAA},
  publisher	= springer,
  series	= lncs,
  volume	= {5642},
  year		= {2009},
  isbn		= {978-3-642-02978-3},
  ee		= {https://doi.org/10.1007/978-3-642-02979-0},
  bibsource	= {DBLP, http://dblp.uni-trier.de}
}

@Book{		  dijk76,
  author	= "E. W. Dijkstra",
  title		= "A Discipline of Programming",
  publisher	= "Prentice Hall",
  year		= "1976",
  note		= "Ch. 25"
}

@InProceedings{	  dipe09,
  author	= {de Dios, Javier and Pe{\~n}a, Ricardo},
  title		= {Formal Certification of a Resource-Aware Language
		  Implementation},
  booktitle	= {TPHOLs '09},
  year		= {2009},
  isbn		= {978-3-642-03358-2},
  pages		= {196--211},
  location	= {Munich, Germany},
  publisher	= springer,
  address	= {Berlin, Heidelberg}
}

###InProceedings{ dipe09,
  author	= {de Dios, Javier and Pe{\~n}a, Ricardo},
  title		= {Formal Certification of a Resource-Aware Language
		  Implementation},
  booktitle	= {TPHOLs '09},
  year		= {2009},
  isbn		= {978-3-642-03358-2},
  pages		= {196--211},
  location	= {Munich, Germany},
  doi		= {https://doi.org/10.1007/978-3-642-03359-9_15},
  publisher	= springer,
  address	= {Berlin, Heidelberg}
}

@MastersThesis{	  eberl12,
  title		= {Efficient and Verified Computation of Simulation Relations
		  on {NFA}s},
  author	= {Manuel Eberl},
  school	= {Technische Universit\"at M\"unchen},
  year		= {2012},
  type		= {Bachelor's thesis}
}

@TechReport{	  egl75,
  author	= {Herbert Egli},
  title		= {A mathematical model for nondeterministic computations},
  institution	= {ETH Z{\"u}rich},
  year		= {1975}
}

###TechReport{	  egl75,
  author	= {Herbert Egli},
  title		= {A mathematical model for nondeterministic computations},
  institution	= {ETH Z{\"u}rich},
  year		= {1975}
}
@inproceedings{Neu12,
    author = {Rene Neumann},
    booktitle = {Proc. of the Workshop on Automated Theory Exploration (ATX 2012)},
    editor = {Annabelle McIver and Peter H\"ofner},
    pages = {36--45},
    publisher = {EasyChair},
    title = {A Framework for Verified Depth-First Algorithms},
    year = {2012}
}

@incollection{elnn13,
year={2013},
booktitle={CAV},
volume={8044},
series={LNCS},
title={A Fully Verified Executable {LTL} Model Checker},
publisher={Springer},
author={Esparza, Javier and Lammich, Peter and Neumann, René and Nipkow, Tobias and Schimpf, Alexander and Smaus, Jan-Georg},
pages={463-478}
}

@InProceedings{	  fado09,
  author	= {Andr{\'e} Almeida and Marco Almeida and Jos{\'e} Alves and
		  Nelma Moreira and Rog{\'e}rio Reis},
  title		= {{FAdo} and {GUItar}},
  booktitle	= {CIAA},
  year		= {2009},
  pages		= {65--74},
  crossref	= {DBLP:conf/wia/2009},
  bibsource	= {DBLP, http://dblp.uni-trier.de}
}

###InProceedings{ fado09,
  author	= {Andr{\'e} Almeida and Marco Almeida and Jos{\'e} Alves and
		  Nelma Moreira and Rog{\'e}rio Reis},
  title		= {{FAdo} and {GUItar}},
  booktitle	= {CIAA},
  year		= {2009},
  pages		= {65--74},
  ee		= {https://doi.org/10.1007/978-3-642-02979-0_10},
  crossref	= {DBLP:conf/wia/2009},
  bibsource	= {DBLP, http://dblp.uni-trier.de}
}

@Article{	  Gabow00,
  title		= "Path-based depth-first search for strong and biconnected
		  components ",
  journal	= "Information Processing Letters ",
  volume	= "74",
  number	= "3-4",
  pages		= "107--114",
  year		= "2000",
  author	= "Harold N. Gabow"
}

@InProceedings{	  gerpelvarwol95,
  author	= {Rob Gerth and Doron Peled and Moshe Y. Vardi and Pierre
		  Wolper},
  title		= {Simple on-the-fly automatic verification of linear
		  temporal logic},
  editor	= {Piotr Dembinski and Marek Sredniawa},
  booktitle	= {Proc.\ Int.\ Symp.\ Protocol Specification, Testing, and
		  Verification},
  pages		= {3--18},
  year		= 1996,
  publisher	= {Chapman \& Hall},
  series	= {IFIP Conference Proceedings},
  volume	= {38}
}

###InProceedings{ gerpelvarwol95,
  author	= {Rob Gerth and Doron Peled and Moshe Y. Vardi and Pierre
		  Wolper},
  title		= {Simple on-the-fly automatic verification of linear
		  temporal logic},
  editor	= {Piotr Dembinski and Marek Sredniawa},
  booktitle	= {Proc.\ Int.\ Symp.\ Protocol Specification, Testing, and
		  Verification},
  pages		= {3--18},
  year		= 1996,
  publisher	= {Chapman \& Hall},
  series	= {IFIP Conference Proceedings},
  volume	= {38}
}

@Article{	  geva05,
  author	= {Geldenhuys, Jaco and Valmari, Antti},
  title		= {More Efficient On-the-fly {LTL} Verification with {T}arjan's
		  Algorithm},
  journal	= {Theor. Comput. Sci.},
  volume	= {345},
  number	= {1},
  month		= nov,
  year		= {2005},
  issn		= {0304-3975},
  pages		= {60--82},
  publisher	= {Elsevier},
}

@Book{		  gome93,
  author	= {M.J.C. Gordon and T.F. Melham},
  title		= {Introduction to {HOL}: A Theorem Proving Environment for
		  Higher Order Logic},
  publisher	= {Cambridge University},
  key		= {GoMe93},
  year		= 1993
}

###Book{	  gome93,
  author	= {M.J.C. Gordon and T.F. Melham},
  title		= {Introduction to {HOL}: A Theorem Proving Environment for
		  Higher Order Logic},
  publisher	= {Cambridge University},
  key		= {GoMe93},
  year		= 1993
}

@PhDThesis{	  haft09,
  author	= {Florian Haftmann},
  title		= {Code Generation from Specifications in Higher Order
		  Logic},
  school	= {Technische Universit\"at M\"unchen},
  year		= {2009}
}

###PhDThesis{	  haft09,
  author	= {Florian Haftmann},
  title		= {Code Generation from Specifications in Higher Order
		  Logic},
  school	= {Technische Universit\"at M\"unchen},
  year		= {2009}
}

@InProceedings{	  haft10,
  author	= {Florian Haftmann and Tobias Nipkow},
  title		= {Code Generation via Higher-Order Rewrite Systems},
  booktitle	= {Functional and Logic Programming (FLOPS 2010)},
  series	= lncs,
  year		= {2010},
  publisher	= springer
}

@Misc{		  haft10b,
  author	= {Florian Haftmann},
  title		= {Data Refinement (Raffinement) in {Isabelle/HOL}},
  year		= {2010},
  note		= {Available at \url{https://isabelle.in.tum.de/community/}}
}

###Misc{	  haft10b,
  author	= {Florian Haftmann},
  title		= {Data Refinement (Raffinement) in {Isabelle/HOL}},
  year		= {2010},
  note		= {Available at \url{https://isabelle.in.tum.de/community/}}
}

@InProceedings{	  haftmannnipkow:2010:codegeneration,
  author	= {Florian Haftmann and Tobias Nipkow},
  title		= {Code Generation via Higher-Order Rewrite Systems},
  booktitle	= {Functional and Logic Programming (FLOPS)},
  year		= {2010},
  editor	= {Matthias Blume and Naoki Kobayashi and Germ{\'a}n Vidal},
  volume	= {6009},
  pages		= {103--117},
  series	= lncs,
  publisher	= springer
}

###InProceedings{ haftmannnipkow:2010:codegeneration,
  author	= {Florian Haftmann and Tobias Nipkow},
  title		= {Code Generation via Higher-Order Rewrite Systems},
  booktitle	= flops,
  year		= {2010},
  editor	= {Matthias Blume and Naoki Kobayashi and Germ{\'a}n Vidal},
  volume	= {6009},
  pages		= {103--117},
  series	= lncs,
  publisher	= springer
}

@InProceedings{	  hani10,
  author	= {Florian Haftmann and Tobias Nipkow},
  title		= {Code Generation via Higher-Order Rewrite Systems},
  booktitle	= {Functional and Logic Programming (FLOPS 2010)},
  series	= lncs,
  year		= {2010},
  publisher	= springer
}

###InProceedings{ hani10,
  author	= {Florian Haftmann and Tobias Nipkow},
  title		= {Code Generation via Higher-Order Rewrite Systems},
  booktitle	= {Functional and Logic Programming (FLOPS 2010)},
  series	= lncs,
  year		= {2010},
  publisher	= springer
}

@Article{	  hardy:ramanujan:1917:qjm,
  author	= "G. H. Hardy and S. Ramanujan",
  title		= "The normal number of prime factors of a number",
  journal	= "Quart. J. of Math.",
  volume	= 48,
  pages		= "76--92",
  year		= "1917"
}

###Article{	  hardy:ramanujan:1917:qjm,
  author	= "G. H. Hardy and S. Ramanujan",
  title		= "The normal number of prime factors of a number",
  journal	= "Quart. J. of Math.",
  volume	= 48,
  pages		= "76--92",
  year		= "1917"
}

@Misc{		  hkkn13,
  title		= {Data Refinement in {Isabelle/HOL}},
  author	= {Florian Haftmann and Alexander Krauss and Ond\v{r}ej
		  Kun\v{c}ar and Tobias Nipkow},
  year		= {2013},
  note		= {To appear in Proc. of ITP 2013}
}

@Article{	  hoa69,
  author	= {Hoare, C. A. R.},
  title		= {An axiomatic basis for computer programming},
  journal	= {Commun. ACM},
  volume	= 12,
  issue		= 10,
  month		= {October},
  year		= 1969,
  pages		= {576--580},
  numpages	= 5,
  publisher	= {ACM},
  address	= {New York, NY, USA}
}

###Article{	  hoa69,
  author	= {Hoare, C. A. R.},
  title		= {An axiomatic basis for computer programming},
  journal	= {Commun. ACM},
  volume	= 12,
  issue		= 10,
  month		= {October},
  year		= 1969,
  pages		= {576--580},
  numpages	= 5,
  publisher	= {ACM},
  address	= {New York, NY, USA}
}

@Article{	  hoa72,
  author	= {Hoare, C. A. R.},
  title		= {Proof of correctness of data representations},
  journal	= {Acta Informatica},
  publisher	= springer,
  keyword	= {Computer Science},
  pages		= {271--281},
  volume	= {1},
  issue		= {4},
  year		= {1972}
}

###Article{	  hoa72,
  author	= {Hoare, C. A. R.},
  title		= {Proof of correctness of data representations},
  journal	= {Acta Informatica},
  publisher	= springer,
  issn		= {0001-5903},
  keyword	= {Computer Science},
  pages		= {271--281},
  volume	= {1},
  issue		= {4},
  url		= {https://doi.org/10.1007/BF00289507},
  note		= {10.1007/BF00289507},
  year		= {1972}
}

@Book{		  holzmann03,
  author	= "Gerard J. Holzmann",
  title		= "The Spin Model Checker --- Primer and Reference Manual",
  publisher	= "Addison-Wesley",
  year		= 2003
}

###Book{	  holzmann03,
  author	= "Gerard J. Holzmann",
  title		= "The Spin Model Checker --- Primer and Reference Manual",
  publisher	= "Addison-Wesley",
  year		= 2003
}

@InProceedings{	  holzmannpeledetal:1997:nesteddfs,
  author	= {Gerard Holzmann and Doron Peled and Mihalis Yannakakis},
  title		= {On Nested Depth First Search},
  booktitle	= {Proc. of SPIN Workshop},
  year		= {1997},
  volume	= {32},
  series	= {Discrete Mathematics and Theoretical Computer Science},
  pages		= {23--32},
  publisher	= {American Mathematical Society}
}

###InProceedings{ holzmannpeledetal:1997:nesteddfs,
  author	= {Gerard Holzmann and Doron Peled and Mihalis Yannakakis},
  title		= {On Nested Depth First Search},
  booktitle	= {Proc. of the 2nd SPIN Workshop},
  year		= {1997},
  editor	= {Jean-Charles Gr\'{e}goire and Gerard J. Holzmann and Doron
		  A. Peled},
  volume	= {32},
  series	= {Discrete Mathematics and Theoretical Computer Science},
  pages		= {23--32},
  publisher	= {American Mathematical Society}
}

@InProceedings{	  hom09,
  title		= {The {HOL}-{O}mega Logic},
  author	= {Peter V. Homeier},
  booktitle	= {Proc. of TPHOLs},
  year		= {2009},
  publisher	= springer,
  volume	= {5674},
  pages		= {244--259},
  series	= lncs
}

@InCollection{	  hop71,
  author	= {John E. Hopcroft},
  title		= {An $n\log n$ algorithm for minimizing the states in a
		  finite automaton},
  booktitle	= {Theory of Machines and Computations},
  year		= {1971},
  publisher	= {Academic Press},
  pages		= {189--196}
}

###InCollection{  hop71,
  author	= {John E. Hopcroft},
  title		= {An $n\log n$ algorithm for minimizing the states in a
		  finite automaton},
  booktitle	= {Theory of Machines and Computations},
  year		= {1971},
  publisher	= {Academic Press},
  pages		= {189--196}
}

@Misc{		  huku12,
  title		= {Lifting and Transfer: A Modular Design for Quotients in
		  {Isabelle/HOL}},
  author	= {Brian Huffman and Ondřej Kunčar},
  year		= {2012},
  note		= {Isabelle Users Workshop 2012}
}

@InCollection{	  iny04,
  year		= {2004},
  booktitle	= {Theory Is Forever},
  volume	= {3113},
  series	= lncs,
  title		= {On {NFA} Reductions},
  publisher	= springer,
  author	= {Ilie, Lucian and Navarro, Gonzalo and Yu, Sheng},
  pages		= {112-124}
}

@Misc{		  javacollfr,
  key		= "Java Collections Framework",
  title		= {{J}ava: The Collections Framework},
  url		= {http://java.sun.com/javase/6/docs/technotes/
		  guides/collections/}
}

###Misc{	  javacollfr,
  key		= "Java Collections Framework",
  title		= {Java: The Collections Framework},
  url		= {http://java.sun.com/javase/6/docs/technotes/
		  guides/collections/}
}

@Article{	  kamo97,
  author	= {Matt Kaufmann and J. Strother Moore},
  title		= {An Industrial Strength Theorem Prover for a Logic Based on
		  {C}ommon {L}isp},
  journal	= {IEEE Transactions on Software Engineering},
  year		= {1997},
  volume	= {23},
  pages		= {203--213}
}

###Article{	  kamo97,
  author	= {Matt Kaufmann and J. Strother Moore},
  title		= {An Industrial Strength Theorem Prover for a Logic Based on
		  Common Lisp},
  journal	= {IEEE Transactions on Software Engineering},
  year		= {1997},
  volume	= {23},
  pages		= {203--213}
}

@InProceedings{	  kleinehacdeeknstw09,
  author	= {Gerwin Klein and Kevin Elphinstone and Gernot Heiser and
		  June Andronick and David Cock and Philip Derrin and
		  Dhammika Elkaduwe and Kai Engelhardt and Rafal Kolanski and
		  Michael Norrish and Thomas Sewell and Harvey Tuch and Simon
		  Winwood},
  title		= {{seL4}: formal verification of an {OS} kernel},
  booktitle	= {Proc.\ ACM Symp.\ Operating Systems Principles},
  year		= {2009},
  pages		= {207--220},
  editor	= {Jeanna Neefe Matthews and Thomas E. Anderson},
  publisher	= {ACM}
}

###InProceedings{ kleinehacdeeknstw09,
  author	= {Gerwin Klein and Kevin Elphinstone and Gernot Heiser and
		  June Andronick and David Cock and Philip Derrin and
		  Dhammika Elkaduwe and Kai Engelhardt and Rafal Kolanski and
		  Michael Norrish and Thomas Sewell and Harvey Tuch and Simon
		  Winwood},
  title		= {{seL4}: formal verification of an {OS} kernel},
  booktitle	= {Proc.\ ACM Symp.\ Operating Systems Principles},
  year		= {2009},
  pages		= {207--220},
  editor	= {Jeanna Neefe Matthews and Thomas E. Anderson},
  publisher	= {ACM}
}

@Article{	  kleinn-toplas,
  author	= {Gerwin Klein and Tobias Nipkow},
  title		= {A Machine-Checked Model for a {Java}-Like Language,
		  Virtual Machine and Compiler},
  journal	= toplas,
  volume	= {28},
  number	= {4},
  year		= {2006},
  pages		= {619--695}
}

###Article{	  kleinn-toplas,
  author	= {Gerwin Klein and Tobias Nipkow},
  title		= {A Machine-Checked Model for a {Java}-Like Language,
		  Virtual Machine and Compiler},
  journal	= toplas,
  volume	= {28},
  number	= {4},
  year		= {2006},
  pages		= {619--695}
}

@InProceedings{	  kr10,
  author	= {Alexander Krauss},
  title		= {Recursive definitions of monadic functions},
  booktitle	= {Proc. of PAR},
  volume	= {43},
  pages		= {1--13},
  year		= {2010}
}

###InProceedings{ kr10,
  author	= {Alexander Krauss},
  title		= {Recursive definitions of monadic functions},
  booktitle	= {Proc. of PAR},
  volume	= {43},
  pages		= {1--13},
  year		= {2010}
}

@InCollection{	  kun04,
  author	= {Viktor Kuncak},
  title		= {Binary Search Trees},
  booktitle	= {Archive of Formal Proofs},
  editor	= {Gerwin Klein and Tobias Nipkow and Lawrence Paulson},
  publisher	= {\url{http://isa-afp.org/entries/BinarySearchTree.shtml}},
  month		= apr,
  year		= 2004,
  note		= {Formal proof development},
  issn		= {2150-914x}
}

###InCollection{  kun04,
  author	= {Viktor Kuncak},
  title		= {Binary Search Trees},
  booktitle	= {Archive of Formal Proofs},
  editor	= {Gerwin Klein and Tobias Nipkow and Lawrence Paulson},
  publisher	= {\url{http://isa-afp.org/entries/BinarySearchTree.shtml}},
  month		= apr,
  year		= 2004,
  note		= {Formal proof development},
  issn		= {2150-914x}
}

@InCollection{	  l09_collections,
  author	= {Peter Lammich},
  title		= {Collections Framework},
  booktitle	= {Archive of Formal Proofs},
  publisher	= {\url{http://isa-afp.org/entries/Collections.shtml}},
  month		= dec,
  year		= 2009,
  note		= {Formal proof development},
  issn		= {2150-914x}
}

###InCollection{  l09_collections,
  author	= {Peter Lammich},
  title		= {Collections Framework},
  booktitle	= {Archive of Formal Proofs},
  publisher	= {\url{http://isa-afp.org/entries/Collections.shtml}},
  month		= dec,
  year		= 2009,
  note		= {Formal proof development},
  issn		= {2150-914x}
}

@InCollection{	  l09_tree_automata,
  author	= {Peter Lammich},
  title		= {Tree Automata},
  booktitle	= {Archive of Formal Proofs},
  publisher	= {\url{http://isa-afp.org/entries/Tree-Automata.shtml}},
  month		= dec,
  year		= {2009},
  note		= {Formal proof development},
  issn		= {2150-914x}
}

###InCollection{  l09_tree_automata,
  author	= {Peter Lammich},
  title		= {Tree Automata},
  booktitle	= {Archive of Formal Proofs},
  publisher	= {\url{http://isa-afp.org/entries/Tree-Automata.shtml}},
  month		= dec,
  year		= {2009},
  note		= {Formal proof development},
  issn		= {2150-914x}
}

@InCollection{	  la12,
  author	= {Peter Lammich},
  title		= {Refinement for Monadic Programs},
  booktitle	= {Archive of Formal Proofs},
  publisher	= {\url{http://isa-afp.org/entries/Refine\_Monadic.shtml}},
  year		= {2012},
  note		= {Formal proof development}
}

###InCollection{  la12,
  author	= {Peter Lammich},
  title		= {Refinement for Monadic Programs},
  booktitle	= {Archive of Formal Proofs},
  publisher	= {\url{http://isa-afp.org/entries/Refine\_Monadic.shtml}},
  year		= {2012},
  note		= {Formal proof development}
}

@InCollection{	  la13,
  year		= {2013},
  booktitle	= {Interactive Theorem Proving},
  volume	= {7998},
  series	= {LNCS},
  title		= {Automatic Data Refinement},
  publisher	= {Springer Berlin Heidelberg},
  author	= {Lammich, Peter},
  pages		= {84-99}
}

@InProceedings{	  latu12,
  author	= {Peter Lammich and Thomas Tuerk},
  title		= {Applying Data Refinement for Monadic Programs to
		  {H}opcroft's Algorithm},
  booktitle	= {Proc. of ITP},
  year		= {2012},
  publisher	= springer,
  volume	= {7406},
  pages		= {166--182},
  series	= lncs
}

###InProceedings{ latu12,
  author	= {Peter Lammich and Thomas Tuerk},
  title		= {Applying Data Refinement for Monadic Programs to
		  {H}opcroft's Algorithm},
  booktitle	= itp,
  year		= {2012},
  publisher	= springer,
  volume	= {7406},
  pages		= {166--182},
  series	= lncs,
  editor	= {Beringer, Lennart and Felty, Amy}
}

@InProceedings{	  lb11,
  title		= {Animating the Formalised Semantics of a {J}ava-like
		  Language},
  booktitle	= {Proc. of ITP},
  year		= {2011},
  publisher	= springer,
  volume	= {6898},
  pages		= {216--232},
  author	= {Andreas Lochbihler and Lukas Bulwahn},
  series	= lncs
}

###InProceedings{ lb11,
  title		= {Animating the Formalised Semantics of a Java-like
		  Language},
  booktitle	= {Interactive Theorem Proving (ITP)},
  year		= {2011},
  publisher	= springer,
  volume	= {6898},
  pages		= {216--232},
  author	= {Andreas Lochbihler and Lukas Bulwahn},
  series	= lncs
}

@Article{	  leroy-jar09,
  author	= {Xavier Leroy},
  title		= {A Formally Verified Compiler Back-end},
  journal	= {J. Automated Reasoning},
  year		= 2009,
  volume	= 43,
  pages		= {363--446}
}

###Article{	  leroy-jar09,
  author	= {Xavier Leroy},
  title		= {A Formally Verified Compiler Back-end},
  journal	= {J. Automated Reasoning},
  year		= 2009,
  volume	= 43,
  pages		= {363--446}
}

@Misc{		  lethal,
  key		= "Lethal",
  title		= "{LETHAL} Tree and Hedge Automata Library",
  url		= "http://lethal.sourceforge.net/"
}

###Misc{	  lethal,
  key		= "Lethal",
  title		= "{LETHAL} Tree and Hedge Automata Library",
  url		= "http://lethal.sourceforge.net/"
}

@InProceedings{	  ll10,
  author	= {P. Lammich and A. Lochbihler},
  title		= {The {Isabelle} {Collections} {Framework}},
  booktitle	= {Proc. of ITP},
  series	= lncs,
  publisher	= springer,
  pages		= {339--354},
  volume	= {6172},
  year		= {2010}
}

###InProceedings{ ll10,
  author	= {P. Lammich and A. Lochbihler},
  title		= {The {Isabelle} {Collections} {Framework}},
  booktitle	= itp,
  series	= lncs,
  publisher	= springer,
  pages		= {339--354},
  volume	= {6172},
  year		= {2010},
  editor	= {Kaufmann, Matt and Paulson, Lawrence C.}
}

@Book{		  lncs2283,
  author	= {Tobias Nipkow and Lawrence Paulson and Markus Wenzel},
  title		= {{Isabelle/HOL} --- A Proof Assistant for Higher-Order
		  Logic},
  publisher	= springer,
  series	= lncs,
  volume	= 2283,
  year		= 2002
}

###Book{	  lncs2283,
  author	= {Tobias Nipkow and Lawrence Paulson and Markus Wenzel},
  title		= "Isabelle/HOL --- A Proof Assistant for Higher-Order Logic",
  publisher	= springer,
  series	= lncs,
  volume	= 2283,
  year		= 2002
}

@InProceedings{	  lrw95,
  author	= {Thomas Langbacka and Rimvydas Ruksenas and Joakim von
		  Wright},
  title		= {{TkWinHOL}: A Tool for Doing Window Inference in {HOL}},
  booktitle	= {Proc. of International Workshop on Higher Order Logic
		  Theorem Proving and its Applications},
  year		= {1995},
  pages		= {245--260},
  publisher	= springer
}

###InProceedings{ lrw95,
  author	= {Thomas Langbacka and Rimvydas Ruksenas and Joakim von
		  Wright},
  title		= {TkWinHOL: A Tool for Doing Window Inference in HOL},
  booktitle	= {Proc. of International Workshop on Higher Order Logic
		  Theorem Proving and its Applications},
  year		= {1995},
  pages		= {245--260},
  publisher	= springer
}

@InProceedings{	  malechamsw-popl10,
  author	= {G. Malecha and G. Morrisett and A. Shinnar and R.
		  Wisnesky},
  title		= {Toward a verified relational database management system},
  booktitle	= {Principles of Programming Languages (POPL'10)},
  pages		= {237--248},
  year		= 2010,
  publisher	= {ACM}
}

###InProceedings{ malechamsw-popl10,
  author	= {G. Malecha and G. Morrisett and A. Shinnar and R.
		  Wisnesky},
  title		= {Toward a verified relational database management system},
  booktitle	= {Principles of Programming Languages (POPL'10)},
  pages		= {237--248},
  year		= 2010,
  publisher	= {ACM}
}

@Book{		  mmo97,
  author	= {Markus M{\"u}ller-Olm},
  title		= {Modular Compiler Verification {---} A Refinement-Algebraic
		  Approach Advocating Stepwise Abstraction},
  publisher	= springer,
  year		= {1997},
  series	= lncs,
  volume	= {1283}
}

###Book{	  mmo97,
  author	= {Markus M{\"u}ller-Olm},
  title		= {Modular Compiler Verification {---} A Refinement-Algebraic
		  Approach Advocating Stepwise Abstraction},
  publisher	= springer,
  year		= {1997},
  series	= lncs,
  volume	= {1283}
}

@Article{	  morr87,
  title		= {A theoretical basis for stepwise refinement and the
		  programming calculus},
  author	= {Joseph M. Morris},
  journal	= {Science of Computer Programming},
  volume	= {9},
  number	= {3},
  pages		= {287--306},
  year		= {1987}
}

###Article{	  morr87,
  title		= {A theoretical basis for stepwise refinement and the
		  programming calculus},
  author	= {Joseph M. Morris},
  journal	= {Science of Computer Programming},
  volume	= {9},
  number	= {3},
  pages		= {287--306},
  year		= {1987}
}

@InCollection{	  mss86,
  author	= {Melton, A. and Schmidt, D. and Strecker, G.},
  title		= {{G}alois connections and computer science applications},
  booktitle	= {Category Theory and Computer Programming},
  series	= lncs,
  publisher	= springer,
  pages		= {299--312},
  volume	= {240},
  year		= {1986}
}

###InCollection{  mss86,
  author	= {Melton, A. and Schmidt, D. and Strecker, G.},
  title		= {Galois connections and computer science applications},
  booktitle	= {Category Theory and Computer Programming},
  series	= lncs,
  publisher	= springer,
  pages		= {299--312},
  volume	= {240},
  year		= {1986}
}

@Article{	  munro71,
  title		= "Efficient determination of the transitive closure of a
		  directed graph ",
  journal	= "Information Processing Letters ",
  volume	= "1",
  number	= "2",
  pages		= "56 - 58",
  year		= "1971",
  note		= "",
  issn		= "0020-0190",
  author	= "Ian Munro"
}

@InProceedings{	  must89,
  author	= {David R. Musser and Alexander A. Stepanov},
  title		= {Generic Programming},
  booktitle	= {Proc. of ISSAC},
  year		= {1989},
  publisher	= springer,
  volume	= {358},
  pages		= {13--25},
  series	= lncs
}

@InProceedings{	  myow12,
  author	= {Myreen, Magnus O. and Owens, Scott},
  title		= {Proof-producing synthesis of {ML} from higher-order
		  logic},
  booktitle	= {Proceedings of the 17th ACM SIGPLAN international
		  conference on Functional programming},
  series	= {ICFP '12},
  year		= {2012},
  pages		= {115--126},
  publisher	= {ACM}
}

@InProceedings{	  namjoshi01,
  author	= {Kedar S. Namjoshi},
  title		= {Certifying Model Checkers},
  booktitle	= cav,
  year		= {2001},
  pages		= {2--13},
  ee		= {https://doi.org/10.1007/3-540-44585-4_2},
  crossref	= {DBLP:conf/cav/2001},
  bibsource	= {DBLP, http://dblp.uni-trier.de}
}

@InCollection{	  nipu04,
  author	= {Tobias Nipkow and Cornelia Pusch},
  title		= {{AVL} Trees},
  booktitle	= {Archive of Formal Proofs},
  editor	= {Gerwin Klein and Tobias Nipkow and Lawrence Paulson},
  publisher	= {\url{http://isa-afp.org/entries/AVL-Trees.shtml}},
  month		= mar,
  year		= 2004,
  note		= {Formal proof development},
  issn		= {2150-914x}
}

###InCollection{  nipu04,
  author	= {Tobias Nipkow and Cornelia Pusch},
  title		= {{AVL} Trees},
  booktitle	= {Archive of Formal Proofs},
  editor	= {Gerwin Klein and Tobias Nipkow and Lawrence Paulson},
  publisher	= {\url{http://isa-afp.org/entries/AVL-Trees.shtml}},
  month		= mar,
  year		= 2004,
  note		= {Formal proof development},
  issn		= {2150-914x}
}

@Misc{		  nola12,
  author	= {Benedikt Nordhoff and Peter Lammich},
  title		= {Formalization of {D}ijkstra's Algorithm},
  booktitle	= {Archive of Formal Proofs},
  publisher	= {\url{http://isa-afp.org/entries/DiskPaxos.shtml}},
  year		= {2012},
  note		= {Formal proof development}
}

###Misc{	  nola12,
  author	= {Benedikt Nordhoff and Peter Lammich},
  title		= {Formalization of {D}ijkstra's Algorithm},
  booktitle	= {Archive of Formal Proofs},
  publisher	= {\url{http://isa-afp.org/entries/DiskPaxos.shtml}},
  year		= {2012},
  note		= {Formal proof development}
}

@Book{		  npw02,
  author	= {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
  title		= {{Isabelle/HOL} --- A Proof Assistant for Higher-Order
		  Logic},
  publisher	= springer,
  series	= lncs,
  volume	= 2283,
  year		= 2002
}

###Book{	  npw02,
  author	= {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
  title		= {Isabelle/HOL --- A Proof Assistant for Higher-Order
		  Logic},
  publisher	= springer,
  series	= lncs,
  volume	= 2283,
  year		= 2002
}

@InCollection{	  old84,
  author	= {Olderog, Ernst-R{\"u}diger},
  title		= {Hoare's logic for programs with procedures --- What has
		  been achieved?},
  booktitle	= {Logics of Programs},
  series	= lncs,
  publisher	= springer,
  pages		= {383-395},
  volume	= {164},
  year		= {1984}
}

###InCollection{  old84,
  author	= {Olderog, Ernst-R{\"u}diger},
  title		= {Hoare's logic for programs with procedures --- What has
		  been achieved?},
  booktitle	= {Logics of Programs},
  series	= lncs,
  publisher	= springer,
  pages		= {383-395},
  volume	= {164},
  year		= {1984}
}

@InProceedings{	  peledpz01,
  author	= {Doron Peled and Amir Pnueli and Lenore D. Zuck},
  title		= {From Falsification to Verification},
  booktitle	= fsttcs,
  year		= {2001},
  pages		= {292--304},
  ee		= {https://doi.org/10.1007/3-540-45294-X_25},
  crossref	= {DBLP:conf/fsttcs/2001},
  bibsource	= {DBLP, http://dblp.uni-trier.de}
}

@InProceedings{	  peyton:jones:1996:fpw,
  author	= "Peyton Jones, Simon",
  title		= "Bulk types with class",
  booktitle	= "FPW '96",
  year		= 1996
}

###InProceedings{ peyton:jones:1996:fpw,
  author	= "Peyton Jones, Simon",
  title		= "Bulk types with class",
  booktitle	= "FPW '96",
  year		= 1996
}

@Article{	  plo76,
  author	= {G. D. Plotkin},
  title		= {A Powerdomain Construction},
  journal	= {SIAM J. Comput.},
  volume	= {5},
  issue		= {3},
  pages		= {452--487},
  year		= {1976}
}

###Article{	  plo76,
  author	= {G. D. Plotkin},
  title		= {A Powerdomain Construction},
  journal	= {SIAM J. Comput.},
  volume	= {5},
  issue		= {3},
  pages		= {452--487},
  year		= {1976}
}

@PhDThesis{	  preo06,
  author	= {Viorel Preoteasa},
  title		= {Program Variables --- The Core of Mechanical Reasoning
		  about Imperative Programs},
  school	= {Turku Centre for Computer Science},
  year		= {2006}
}

###PhDThesis{	  preo06,
  author	= {Viorel Preoteasa},
  title		= {Program Variables --- The Core of Mechanical Reasoning
		  about Imperative Programs},
  school	= {Turku Centre for Computer Science},
  year		= {2006}
}

@Article{	  purdom70,
  year		= {1970},
  issn		= {0006-3835},
  journal	= {BIT Numerical Mathematics},
  volume	= {10},
  number	= {1},
  title		= {A transitive closure algorithm},
  publisher	= {Kluwer Academic Publishers},
  author	= {Purdom, Paul, Jr.},
  pages		= {76-94}
}

@InCollection{	  rdkp13,
  year		= {2013},
  booktitle	= {Logic for Programming, Artificial Intelligence, and
		  Reasoning},
  volume	= {8312},
  series	= {LNCS},
  title		= {Three {SCC}-Based Emptiness Checks for Generalized {B}{\"u}chi
		  Automata},
  publisher	= {Springer},
  author	= {Renault, Etienne and Duret-Lutz, Alexandre and Kordon,
		  Fabrice and Poitrenaud, Denis},
  pages		= {668-682}
}

@InProceedings{	  rey02,
  author	= {John C. Reynolds},
  title		= {Separation Logic: A Logic for Shared Mutable Data
		  Structures},
  booktitle	= {Proc of. Logic in Computer Science (LICS)},
  year		= {2002},
  pages		= {55--74},
  publisher	= {IEEE}
}

###InProceedings{ rey02,
  author	= {John C. Reynolds},
  title		= {Separation Logic: A Logic for Shared Mutable Data
		  Structures},
  booktitle	= {Proc of. Logic in Computer Science (LICS)},
  year		= {2002},
  pages		= {55--74},
  publisher	= {IEEE}
}

@InProceedings{	  rey83,
  author	= {John C. Reynolds},
  title		= {Types, Abstraction and Parametric Polymorphism},
  booktitle	= {IFIP Congress},
  year		= {1983},
  pages		= {513-523}
}

@Book{		  roen98,
  author	= {Willem-Paul de Roever and Kai Engelhardt},
  title		= {Data Refinement: Model-Oriented Proof Methods and their
		  Comparison},
  publisher	= {Cambridge University Press},
  year		= {1998}
}

###Book{	  roen98,
  author	= {Willem-Paul de Roever and Kai Engelhardt},
  title		= {Data Refinement: Model-Oriented Proof Methods and their
		  Comparison},
  publisher	= {Cambridge University Press},
  year		= {1998}
}

@TechReport{	  ruwr97,
  author	= {Rimvydas Ruksenas and Joakim von Wright},
  title		= {A Tool for Data Refinement},
  year		= {1997},
  institution	= {Turku Centre for Computer Science},
  number	= {TUCS Technical Report No 119}
}

###TechReport{	  ruwr97,
  author	= {Rimvydas Ruksenas and Joakim von Wright},
  title		= {A Tool for Data Refinement},
  year		= {1997},
  institution	= {Turku Centre for Computer Science},
  number	= {TUCS Technical Report No 119}
}

@PhDThesis{	  schi06,
  author	= {Norbert Schirmer},
  title		= {Verification of Sequential Imperative Programs in
		  {I}sabelle/{HOL}},
  school	= {Technische Universit\"at M\"unchen},
  year		= {2006}
}

###PhDThesis{	  schi06,
  author	= {Norbert Schirmer},
  title		= {Verification of Sequential Imperative Programs in
		  {I}sabelle/{HOL}},
  school	= {Technische Universit\"at M\"unchen},
  year		= {2006}
}

@InProceedings{	  schm98,
  author	= {Martin Schwenke and Brendan Mahony},
  title		= {The Essence of Expression Refinement},
  booktitle	= {Proc. of International Refinement Workshop and Formal
		  Methods},
  year		= {1998},
  pages		= {324--333}
}

###InProceedings{ schm98,
  author	= {Martin Schwenke and Brendan Mahony},
  title		= {The Essence of Expression Refinement},
  booktitle	= {Proc. of International Refinement Workshop and Formal
		  Methods},
  year		= {1998},
  pages		= {324--333}
}

@InProceedings{	  schmersma09,
  author	= {Alexander Schimpf and Stephan Merz and Jan-Georg Smaus},
  editor	= {S. Berghofer and T. Nipkow and C. Urban and M. Wenzel},
  title		= {Construction of {B}{\"u}chi Automata for {LTL} Model
		  Checking Verified in {I}sabelle/{HOL}},
  booktitle	= {Theorem Proving in Higher Order Logics, TPHOLs 2009},
  year		= 2009,
  pages		= {424--439},
  series	= lncs,
  volume	= {5674},
  publisher	= springer
}

###InProceedings{ schmersma09,
  author	= {Alexander Schimpf and Stephan Merz and Jan-Georg Smaus},
  editor	= {S. Berghofer and T. Nipkow and C. Urban and M. Wenzel},
  title		= {Construction of {B}{\"u}chi Automata for {LTL} Model
		  Checking Verified in {I}sabelle/{HOL}},
  booktitle	= tphols,
  year		= 2009,
  pages		= {424--439},
  series	= lncs,
  volume	= {5674},
  publisher	= springer
}

@InProceedings{	  schwoonesparza:2005:emptinesscomparison,
  author	= {Stefan Schwoon and Javier Esparza},
  title		= {A Note on On-The-Fly Verification Algorithms},
  booktitle	= {Tools and Algorithms for the Construction and Analysis of
		  Systems (TACAS)},
  year		= {2005},
  editor	= {Nicolas Halbwachs and Lenore Zuck},
  volume	= {3440},
  series	= lncs,
  pages		= {174--190},
  publisher	= springer
}

###InProceedings{ schwoonesparza:2005:emptinesscomparison,
  author	= {Stefan Schwoon and Javier Esparza},
  title		= {A Note on On-The-Fly Verification Algorithms},
  booktitle	= tacas,
  year		= {2005},
  editor	= {Nicolas Halbwachs and Lenore Zuck},
  volume	= {3440},
  series	= lncs,
  pages		= {174--190},
  publisher	= springer
}

@Misc{ChAr07,
  author = "Simon Chemouil and Ludovic Arnold",
  title = "Implémentation d'algorithmes génériques sur les graphes en Coq",
  note = "Rapport de stage de master M1",
  url = "https://www.lri.fr/~arnold/projects:coqgraphs"
}

@Book{		  sewa11,
  author	= "Robert Sedgewick and Kevin Wayne",
  title		= "Algorithms",
  publisher	= "Addison-Wesley Professional",
  year		= 2011,
  note		= {4th edition}
}

@Article{	  sharir81,
  author	= {Sharir, M.},
  journal	= {Computers \& Mathematics with Applications},
  month		= jan,
  number	= {1},
  pages		= {67--72},
  title		= {{A strong-connectivity algorithm and its applications in
		  data flow analysis}},
  volume	= {7},
  year		= {1981}
}

@InProceedings{	  slindn08,
  author	= {Konrad Slind and Michael Norrish},
  title		= {A Brief Overview of {HOL4}},
  booktitle	= {TPHOLs},
  year		= 2008,
  pages		= {28--32},
  ee		= {https://doi.org/10.1007/978-3-540-71067-7_6},
  crossref	= {DBLP:conf/tphol/2008},
  bibsource	= {DBLP, http://dblp.uni-trier.de}
}

###InProceedings{ slindn08,
  author	= {Konrad Slind and Michael Norrish},
  title		= {A Brief Overview of {HOL4}},
  booktitle	= {TPHOLs},
  year		= 2008,
  pages		= {28--32},
  ee		= {https://doi.org/10.1007/978-3-540-71067-7_6},
  crossref	= {DBLP:conf/tphol/2008},
  bibsource	= {DBLP, http://dblp.uni-trier.de}
}

@InProceedings{	  sprengertacas98,
  author	= {Christoph Sprenger},
  title		= {A Verified Model Checker for the Modal $\mu$-Calculus in
		  {Coq}},
  booktitle	= tacas,
  publisher	= springer,
  series	= lncs,
  volume	= 1384,
  year		= 1998,
  pages		= {167--183},
  editor	= {Steffen, Bernhard}
}

@PhDThesis{	  stap99,
  author	= {Mark Staples},
  title		= {A Mechanised Theory of Refinement},
  school	= {University of Cambridge},
  year		= {1999},
  note		= {2nd edition}
}

###PhDThesis{	  stap99,
  author	= {Mark Staples},
  title		= {A Mechanised Theory of Refinement},
  school	= {University of Cambridge},
  year		= {1999},
  note		= {2nd edition}
}

@Article{	  tarjan72,
  author	= {Tarjan, R.},
  title		= {Depth-First Search and Linear Graph Algorithms},
  journal	= {SIAM Journal on Computing},
  volume	= {1},
  number	= {2},
  pages		= {146-160},
  year		= {1972},
  doi		= {10.1137/0201010}
}

@Misc{		  timbuk,
  author	= {T. Genet and V. V. T. Tong},
  title		= {{T}imbuk 2.2},
  url		= {http://www.irisa.fr/celtique/genet/timbuk/}
}

###Misc{	  timbuk,
  author	= {T. Genet and V. V. T. Tong},
  title		= {Timbuk 2.2},
  url		= {http://www.irisa.fr/celtique/genet/timbuk/}
}

@Article{	  vawo94,
  author	= {Moshe Y. Vardi and Pierre Wolper},
  title		= {Reasoning about Infinite Computations},
  journal	= {Information and Computation},
  year		= {1994},
  volume	= {115},
  pages		= {1--37}
}

@inproceedings{VaWo86,
  author = {Vardi, {M.Y.} and Wolper, {P.}},
  booktitle = {In Proceedings of the 1st Symposium on Logic in Computer Science},
  pages = {322--331},
  title = {An automata-theoretic approach to automatic program verification},
  year = 1986
}


@InProceedings{	  wad89,
  author	= {Philip Wadler},
  title		= {Theorems for free!},
  booktitle	= {Proc. of FPCA},
  year		= {1989},
  pages		= {347--359},
  publisher	= {ACM}
}

@InProceedings{	  wad92,
  author	= {Philip Wadler},
  title		= {Comprehending Monads},
  booktitle	= {Mathematical Structures in Computer Science},
  year		= {1992},
  pages		= {61--78}
}

###Article{	  wad92,
  author	= {Philip Wadler},
  title		= {Comprehending Monads},
  journal	= {Mathematical Structures in Computer Science},
  year		= {1992},
  pages		= {461--478},
  volume	= {2},
  issue		= {04}
}

@TechReport{	  wat93,
  author	= {Bruce W. Watson},
  title		= {A taxonomy of finite automata minimization algorithms},
  institution	= {Eindhoven University of Technology, The Netherlands},
  year		= 1993,
  type		= {Comp. Sci. Note},
  number	= {93/44},
  issn		= "0926-4515"
}

###TechReport{	  wat93,
  author	= {Bruce W. Watson},
  title		= {A taxonomy of finite automata minimization algorithms},
  institution	= {Eindhoven University of Technology, The Netherlands},
  year		= 1993,
  type		= {Comp. Sci. Note},
  number	= {93/44},
  issn		= "0926-4515"
}

@InProceedings{	  wri94,
  author	= {J. von Wright},
  title		= {Program Refinement by Theorem Prover},
  booktitle	= {In BCS FACS Sixth Refinement Workshop -- Theory and
		  Practise of Formal Software Development},
  year		= {1994},
  publisher	= springer
}

###InProceedings{ wri94,
  author	= {J. von Wright},
  title		= {Program Refinement by Theorem Prover},
  booktitle	= {In BCS FACS Sixth Refinement Workshop -- Theory and
		  Practise of Formal Software Development},
  year		= {1994},
  publisher	= springer
}
