@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{zhan16,
  author = {Bohua Zhan},
  title = {AUTO2: a saturation-based heuristic prover for higher-order logic},
  booktitle = {{ITP} 2016},
  pages = "441--456",
  editor = "J. C. Blanchette and S. Merz",
  year = {2016}
}

@article{pelletier,
  author = {Francis Jeffry Pelletier},
  title = {Seventy-Five Problems for Testing Automatic Theorem Provers},
  journal = "Journal of Automated Reasoning",
  year = "1986",
  volume = "2",
  pages = "191--216"
}

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