@STRING{LNCS = {LNCS}}
@STRING{Springer = {Springer}}

@article{EFS56,
  doi = {10.1109/tit.1956.1056816},
  url = {https://doi.org/10.1109%2Ftit.1956.1056816},
  year  = {1956},
  month = {dec},
  publisher = {{IEEE}},
  volume = {2},
  number = {4},
  pages = {117--119},
  author = {P. Elias and A. Feinstein and C. Shannon},
  title = {A note on the maximum flow through a network},
  journal = {{IEEE} Transactions on Information Theory}
}



@inproceedings{LaSe16,
  author    = {Peter Lammich and S. Reza Sefidgar},
  title     = {Formalizing the Edmonds-Karp Algorithm},
  booktitle = {Interactive Theorem Proving},
  publisher = Springer,
  year      = {2016},
  note      = {to appear}
}


@inproceedings{LeRu07,
 author = {Lee, Gilbert and Rudnicki, Piotr},
 title = {Alternative Aggregates in Mizar},
 booktitle = {Calculemus '07 / MKM '07},
 year = {2007},
 pages = {327--341},
 numpages = {15},
 publisher = {Springer},
} 

@book{BeCa10,
 author = {Bertot, Yves and Castran, Pierre},
 title = {Interactive Theorem Proving and Program Development: Coq'Art The Calculus of Inductive Constructions},
 year = {2010},
 edition = {1st},
 publisher = Springer,
} 


@inproceedings{La16,
  author    = {Peter Lammich},
  title     = {Refinement based verification of imperative data structures},
  booktitle = {{CPP}},
  pages     = {27--36},
  publisher = {{ACM}},
  year      = {2016}
}


@inproceedings{GAK12,
    publisher        = Springer,
    author           = {Greenaway, David and Andronick, June and Klein, Gerwin},
    month            = {aug},
    year             = {2012},
    title            = {Bridging the Gap: Automatic Verified Abstraction of {C}},
    booktitle        = {ITP},
    pages            = {99-115},
  }

@phdthesis{Greenaway15,
    school           = {CSE, UNSW},
    author           = {Greenaway, David},
    month            = {mar},
    year             = {2015},
    keywords         = {isabelle/hol, c verification, autocorres},
    title            = {Automated proof-producing abstraction of C code},
    address          = {Sydney, Australia}
  }

@PHDTHESIS{Nosch15,
    author = {Lars Noschinski},
    title = {Formalizing Graph Theory and Planarity Certificates},
    school = {Fakultät für Informatik, Technische Universität München},
    year = {2015},
    month = {November},
}


@ARTICLE{MaRu05,
    author = {Roman Matuszewski and Piotr Rudnicki},
    title = {Mizar: the first 30 years},
    journal = {Mechanized Mathematics and Its Applications},
    year = {2005},
    pages = {2005}
}

@inproceedings{Wenzel99,
  author    = {Markus Wenzel},
  title     = {Isar - {A} Generic Interpretative Approach to Readable Formal Proof
               Documents},
  booktitle = {TPHOLs'99},
  pages     = {167--184},
  year      = {1999},
  crossref  = {DBLP:conf/tphol/1999},
}

@proceedings{DBLP:conf/tphol/1999,
  title     = {Theorem Proving in Higher Order Logics, 12th International Conference,
               TPHOLs'99, Nice, France, September, 1999, Proceedings},
  series    = LNCS,
  volume    = {1690},
  publisher = Springer,
  year      = {1999},
}



@article{GoTa88,
 author = {Goldberg, Andrew V. and Tarjan, Robert E.},
 title = {A New Approach to the Maximum-flow Problem},
 journal = {J. ACM},
 issue_date = {Oct. 1988},
 volume = {35},
 number = {4},
 month = oct,
 year = {1988},
 publisher = {ACM},
} 

@incollection{Di06,
 author = {Dinitz, Yefim},
 chapter = {Dinitz' Algorithm: The Original Version and Even's Version},
 title = {Theoretical Computer Science},
 year = {2006},
 pages = {218--240},
 numpages = {23},
 publisher = {Springer},
} 

@article{Wirth71,
 author = {Wirth, Niklaus},
 title = {Program Development by Stepwise Refinement},
 journal = {Commun. ACM},
 issue_date = {April 1971},
 volume = {14},
 number = {4},
 month = apr,
 year = {1971},
 publisher = {ACM},
} 

@incollection{La15,
  year={2015},
  booktitle={ITP},
  volume={9236},
  series={LNCS},
  title={Refinement to {Imperative/HOL}},
  publisher={Springer},
  author={Lammich, Peter},
  pages={253-269},
}

@inproceedings{BCHP05,
 author = {Bornat, Richard and Calcagno, Cristiano and O'Hearn, Peter and Parkinson, Matthew},
 title = {Permission Accounting in Separation Logic},
 booktitle = {POPL},
 year = {2005},
 pages = {259--270},
 numpages = {12},
 publisher = {ACM},
} 


@INPROCEEDINGS{MA07,
    author = {Nicolas Marti and Reynald Affeldt},
    title = {A certified verifier for a fragment of Separation logic},
    booktitle = {PPL-Workshop},
    year = {2007}
}

@INPROCEEDINGS{NMSGB08,
  author = {Aleksandar Nanevski and Greg Morrisett and Avi Shinnar and Paul Govereau and Lars Birkedal},
  title = {Ynot: Reasoning with the awkward squad},
  booktitle = {ICFP},
  year = {2008}
}

@inproceedings{KKB12,
  publisher        = {Springer},
  author           = {Klein, Gerwin and Kolanski, Rafal and Boyton, Andrew},
  month            = {Aug},
  year             = {2012},
  title            = {Mechanised Separation Algebra},
  booktitle        = {ITP},
  pages            = {332-337},
}

@InProceedings{char11,
   author = "Arthur Chargu{\'e}raud",
   title = "Characteristic Formulae for the Verification of Imperative Programs",
   year = "2011",
   pages = "418--430",
   publisher = "ACM",
   booktitle = "ICFP",
}

@incollection{La14,
  year={2014},
  booktitle={ITP},
  volume={8558},
  series={LNCS},
  title={Verified Efficient Implementation of {G}abow’s Strongly Connected Component Algorithm},
  publisher={Springer},
  author={Lammich, Peter},
  pages={325-340},
}


@article{HiPa06,
  title = "Finger Trees: A Simple General-purpose Data Structure",
  author = "Ralf Hinze and Ross Paterson",
  journal = "Journal of Functional Programming",
  volume = 16,
  number = 2,
  pages = "197-217",
  year = 2006
}


@incollection{Pe07,
  year={2007},
  booktitle={Model Checking Software},
  series={LNCS},
  title={BEEM: Benchmarks for Explicit Model Checkers},
  publisher={Springer},
  author={Pelánek, Radek},
  pages={263-267},
}


@inproceedings{CDHY09,
 author = {Calcagno, Cristiano and Distefano, Dino and O'Hearn, Peter and Yang, Hongseok},
 title = {Compositional Shape Analysis by Means of Bi-abduction},
 booktitle = {POPL '09},
 year = {2009},
 pages = {289--300},
} 

@inproceedings{Neu12,
    author = {Rene Neumann},
    booktitle = {Workshop on Automated Theory Exploration (ATX 2012)},
    pages = {36--45},
    title = {A Framework for Verified Depth-First Algorithms},
    year = {2012}
}


@article{LaMe12,
  author  = {Peter Lammich and Rene Meis},
  title   = {A Separation Logic Framework for Imperative HOL},
  journal = {Archive of Formal Proofs},
  month   = nov,
  year    = 2012,
  note    = {\url{https://isa-afp.org/entries/Separation_Logic_Imperative_HOL.shtml},
            Formal proof development},
  ISSN    = {2150-914x},
}

@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}
}


@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}
}

@article{GeVa05,
 author = {Geldenhuys, Jaco and Valmari, Antti},
 title = {More Efficient On-the-fly {LTL} Verification with Tarjan's Algorithm},
 journal = {Theor. Comput. Sci.},
 issue_date = {21 November 2005},
 volume = {345},
 number = {1},
 month = nov,
 year = {2005},
 issn = {0304-3975},
 pages = {60--82},
 numpages = {23},
 url = {https://doi.org/10.1016/j.tcs.2005.07.004},
 doi = {10.1016/j.tcs.2005.07.004},
 acmid = {1121853},
 publisher = {Elsevier Science Publishers Ltd.},
 address = {Essex, UK},
 keywords = {model checking, verification},
}



@inproceedings{CDP05,
 author = {Couvreur, Jean-Michel and Duret-Lutz, Alexandre and Poitrenaud, Denis},
 title = {On-the-fly Emptiness Checks for Generalized B\&\#252;Chi Automata},
 booktitle = {Proceedings of the 12th International Conference on Model Checking Software},
 series = {SPIN'05},
 year = {2005},
 isbn = {3-540-28195-9, 978-3-540-28195-5},
 location = {San Francisco, CA},
 pages = {169--184},
 numpages = {16},
 url = {https://doi.org/10.1007/11537328_15},
 doi = {10.1007/11537328_15},
 acmid = {2156363},
 publisher = {Springer-Verlag},
 address = {Berlin, Heidelberg},
}



@incollection{RDKP13,
year={2013},
isbn={978-3-642-45220-8},
booktitle={Logic for Programming, Artificial Intelligence, and Reasoning},
volume={8312},
series={Lecture Notes in Computer Science},
editor={McMillan, Ken and Middeldorp, Aart and Voronkov, Andrei},
doi={10.1007/978-3-642-45221-5_44},
title={Three SCC-Based Emptiness Checks for Generalized Büchi Automata},
url={https://doi.org/10.1007/978-3-642-45221-5_44},
publisher={Springer Berlin Heidelberg},
author={Renault, Etienne and Duret-Lutz, Alexandre and Kordon, Fabrice and Poitrenaud, Denis},
pages={668-682}
}
@article{Purdom70,
year={1970},
issn={0006-3835},
journal={BIT Numerical Mathematics},
volume={10},
number={1},
doi={10.1007/BF01940892},
title={A transitive closure algorithm},
url={https://doi.org/10.1007/BF01940892},
publisher={Kluwer Academic Publishers},
author={Purdom, Paul, Jr.},
pages={76-94},
language={English}
}

@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",
}

@article{ChMe96,
year={1996},
issn={0178-4617},
journal={Algorithmica},
volume={15},
number={6},
doi={10.1007/BF01940880},
title={Algorithms for dense graphs and networks on the random access computer},
url={https://doi.org/10.1007/BF01940880},
publisher={Springer-Verlag},
keywords={Graph; Network; Algorithm; Dense graph; Dense network},
author={Cheriyan, J. and Mehlhorn, K.},
pages={521-549},
language={English}
}

@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",
note = "",
issn = "0020-0190",
doi = "https://doi.org/10.1016/S0020-0190(00)00051-X",
url = "http://www.sciencedirect.com/science/article/pii/S002001900000051X",
author = "Harold N. Gabow",
}


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


@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}
}



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

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

@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}
} 

@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}
}

@phdthesis{huff12,
  author = {Brian Huffman},
  title = {HOLCF '11: A Definitional Domain Theory for Verifying Functional Programs},
  school = {Portland State University},
  year = {2012}
}

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

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

@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}
}


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

@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}
}


@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}
}


@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}
}

@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{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{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{La13,
year={2013},
booktitle={ITP},
volume={7998},
series={LNCS},
title={Automatic Data Refinement},
publisher={Springer},
author={Lammich, Peter},
pages={84-99}
}

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


@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
}

@TechReport{Tu11,
  author =   {Tuerk, Thomas},
  title =    {{A separation logic framework for HOL}},
  year =   2011,
  month =    jun,
  url =    {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-799.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  number =   {UCAM-CL-TR-799}
}

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

@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{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{Leroy-JAR09,author={Xavier Leroy},
title={A Formally Verified Compiler Back-end},
journal={J. Automated Reasoning},year=2009,volume=43,pages={363--446}}

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


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

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

@incollection{La12,
  author = {Peter Lammich},
  title = {Refinement for Monadic Programs},
  booktitle =    {Archive of Formal Proofs},
  publisher =    {\url{https://isa-afp.org/entries/Refine\_Monadic.shtml}},
  year = {2012},
  note = {Formal proof development}
}
  
@article{NoLa12,
  author = {Benedikt Nordhoff and Peter Lammich},
  title = {Formalization of {D}ijkstra's Algorithm},
  journal =  {Archive of Formal Proofs},
  month =    Jan,
  year =     2012,
  note =     {\url{https://isa-afp.org/entries/Dijkstra_Shortest_Path.shtml}, Formal proof development},
  ISSN =     {2150-914x}
}

@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 = {TPHOL},
 year = {2008},
 pages = {134--149},
 numpages = {16},
 publisher = Springer,
 series    = LNCS,
 volume    = {5170},
}

@book{BaWr98,
  author  =   {Ralph-Johan Back and Joakim von Wright},
  title   =   {Refinement Calculus --- A Systematic Introduction},
  publisher = Springer,
  year      = {1998}
}

@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}
}

@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}
}

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

@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}
}

@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
}

@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}
}

@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
}


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

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

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


@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{Preo06,
  author=  {Viorel Preoteasa},
  title=   {Program Variables --- The Core of Mechanical Reasoning about Imperative Programs},
  school=  {Turku Centre for Computer Science},
  year=    {2006}
}

@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{https://isa-afp.org/entries/Presburger-Automata.shtml}},
  month =        Dec,
  year =         2009,
  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{https://isa-afp.org/entries/BinarySearchTree.shtml}},
  month =        Apr,
  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{https://isa-afp.org/entries/AVL-Trees.shtml}},
  month =        Mar,
  year =         2004,
  note =         {Formal proof development},
  ISSN =         {2150-914x}
}


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


@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}
}

@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)}
}

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

@Misc{MLton,
  key="MLton",
  title = {{MLton} {Standard ML} compiler},
  note = {http://mlton.org/},
  url = {http://mlton.org/}
}

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

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

@misc{Coq:Std:Lib,
  key = "Coq",
  title = "The {Coq} Standard Library",
  url = "http://coq.inria.fr/stdlib/index.html"
}

@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{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"
}

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


@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{Kr10,
  author={Alexander Krauss},
  title={Recursive definitions of monadic functions},
  booktitle={Proc. of PAR},
  volume={43},
  pages={1--13},
  year={2010}
}


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

@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}
}

@inproceedings{HaNi10,
  author     = {Florian Haftmann and Tobias Nipkow},
  title      = {Code Generation via Higher-Order Rewrite Systems},
  booktitle  = {FLOPS 2010},
  series     = LNCS,
  year       = {2010},
  publisher  = Springer
}

@incollection{L09_collections,
  author =       {Peter Lammich},
  title =        {Collections Framework},
  booktitle =    {Archive of Formal Proofs},
  publisher =    {\url{https://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{https://isa-afp.org/entries/Tree-Automata.shtml}},
  month =        Dec,
  year =         {2009},
  note =         {Formal proof development},
  ISSN =         {2150-914x}
}

@INPROCEEDINGS{CHY07,
  author={Calcagno, C. and O'Hearn, P.W. and Hongseok Yang},
  booktitle={LICS 2007},
  title={Local Action and Abstract Separation Logic},
  year={2007},
  month={July},
  pages={366-378},
}

@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}
}

@MasterThesis{Meis2011,
  author={Rene Meis},
  title={{I}ntegration von {S}eparation {L}ogic in das {I}mperative {HOL}-{F}ramework},
  note={Master Thesis, WWU M\"unster},
  year={2011},
  school={WWU M\"unster}
}


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


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

@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"
}

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


@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
}

@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{Bra09,
    author = {Thomas Braibant and Damien Pous},
    title = {A tactic for deciding {K}leene algebras},
    booktitle = {First Coq Workshop},
    year = {2009}
}

@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}
}

@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
}

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

@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}
}


@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{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{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{SE05,
  author = {Stefan Schwoon and Javier Esparza},
  title = {A Note on On-The-Fly Verification Algorithms},
  booktitle = {TACAS},
  year = {2005},
  volume = {3440},
  series = LNCS,
  pages = {174--190},
  publisher = Springer
}

@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
}

@INPROCEEDINGS{HPY96,
  author = {Gerard Holzmann and Doron Peled and Mihalis Yannakakis},
  title = {On Nested Depth First Search},
  booktitle = {SPIN},
  year = {1996},
  volume = {32},
  series = {Discrete Mathematics and Theoretical Computer Science},
  pages = {23--32},
  publisher = {American Mathematical Society}
}

@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/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}
}

@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
}

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

@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
}

@article{FF56,
  title={Maximal flow through a network},
  author={Ford, Lester R and Fulkerson, Delbert R},
  journal={Canadian journal of Mathematics},
  volume={8},
  number={3},
  pages={399--404},
  year={1956}
}

@article{Lee05,
  title={Correctnesss of Ford-Fulkerson’s Maximum Flow Algorithm1},
  author={Lee, Gilbert},
  journal={Formalized Mathematics},
  volume={13},
  number={2},
  pages={305--314},
  year={2005}
}

@book{CLRS09,
 author = {Cormen, Thomas H. and Leiserson, Charles E. and Rivest, Ronald L. and Stein, Clifford},
 title = {Introduction to Algorithms, Third Edition},
 year = {2009},
 edition = {3rd},
 publisher = {The MIT Press},
} 

@article{EK72,
  title={Theoretical improvements in algorithmic efficiency for network flow problems},
  author={Edmonds, Jack and Karp, Richard M},
  journal={J.~ACM},
  volume={19},
  number={2},
  pages={248--264},
  year={1972},
  publisher={ACM}
}

@article{Zwick95,
  title={The smallest networks on which the {F}ord-{F}ulkerson maximum flow procedure may fail to terminate},
  author={Zwick, Uri},
  journal={Theoretical computer science},
  volume={148},
  number={1},
  pages={165--170},
  year={1995},
  publisher={Elsevier}
}
