@inproceedings{zhan18a,
  author = {Bohua Zhan},
  title = {Efficient verification of imperative programs using auto2},
  booktitle = {{TACAS} 2018},
  pages = "23--40",
  editor = "Beyer, Dirk and Huisman, Marieke",
  year = {2018}
}

@InProceedings{imphol,
author="Bulwahn, Lukas
and Krauss, Alexander
and Haftmann, Florian
and Erk{\"o}k, Levent
and Matthews, John",
editor="Mohamed, Otmane Ait
and Mu{\~{n}}oz, C{\'e}sar
and Tahar, Sofi{\`e}ne",
title="Imperative Functional Programming with Isabelle/HOL",
booktitle="Theorem Proving in Higher Order Logics",
year="2008",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="134--149",
isbn="978-3-540-71067-7"
}

@article{Separation_Logic_Imperative_HOL-AFP,
  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{http://isa-afp.org/entries/Separation_Logic_Imperative_HOL.html},
            Formal proof development},
  ISSN    = {2150-914x},
}

@article{prog-prove,
  author = {Tobias Nipkow},
  title = {Programming and Proving in Isabelle/HOL},
  year = 2018,
}

@InProceedings{nipkow16,
author="Nipkow, Tobias",
editor="Blanchette, Jasmin Christian
and Merz, Stephan",
title="Automatic Functional Correctness Proofs for Functional Search Trees",
booktitle="Interactive Theorem Proving",
year="2016",
publisher="Springer International Publishing",
address="Cham",
pages="307--322",
isbn="978-3-319-43144-4"
}
	
@article{Collections-AFP,
  author  = {Peter Lammich},
  title   = {Collections Framework},
  journal = {Archive of Formal Proofs},
  month   = nov,
  year    = 2009,
  note    = {\url{http://isa-afp.org/entries/Collections.html},
            Formal proof development},
  ISSN    = {2150-914x},
}

@article{Dijkstra_Shortest_Path-AFP,
  author  = {Benedikt Nordhoff and Peter Lammich},
  title   = {Dijkstra's Shortest Path Algorithm},
  journal = {Archive of Formal Proofs},
  month   = jan,
  year    = 2012,
  note    = {\url{http://isa-afp.org/entries/Dijkstra_Shortest_Path.html},
            Formal proof development},
  ISSN    = {2150-914x},
}

@article{cormen2009introduction,
  title={Introduction to algorithms third edition},
  author={Cormen, Thomas H and Leiserson, Charles E and Rivest, Ronald L and Stein, Clifford}, 
  year={2009}
}

@article{Refine_Imperative_HOL-AFP,
  author  = {Peter Lammich},
  title   = {The Imperative Refinement Framework},
  journal = {Archive of Formal Proofs},
  month   = aug,
  year    = 2016,
  note    = {\url{http://isa-afp.org/entries/Refine_Imperative_HOL.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
