%  isbn      = {0-201-03822-6},
@book{DBLP:books/aw/Knuth81,
  author    = {Donald E. Knuth},
  title     = {The Art of Computer Programming, Volume {II:} Seminumerical Algorithms,
               2nd Edition},
  publisher = {Addison-Wesley},
  year      = {1981},
  timestamp = {Thu, 03 Jan 2002 11:51:07 +0100},
  biburl    = {http://dblp.uni-trier.de/rec/bib/books/aw/Knuth81},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@article{DBLP:journals/afp/Schirmer08,
  author    = {Norbert Schirmer},
  title     = {A Sequential Imperative Programming Language: Syntax, Semantics, {Hoare}
               Logics and Verification Environment},
  journal   = {Archive of Formal Proofs},
  year      = {2008},
  url       = {http://isa-afp.org/entries/Simpl.shtml},
  timestamp = {Mon, 26 Mar 2012 09:24:33 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/afp/Schirmer08},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@article{DBLP:journals/iandc/MehtaN05,
  author    = {Farhad Mehta and
               Tobias Nipkow},
  title     = {Proving pointer programs in higher-order logic},
  journal   = {Inf. Comput.},
  volume    = {199},
  number    = {1-2},
  pages     = {200--227},
  year      = {2005},
  url       = {https://doi.org/10.1016/j.ic.2004.10.007},
  timestamp = {Wed, 22 Feb 2006 10:52:42 +0100},
  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/iandc/MehtaN05},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@article{Brent:1980,
year={1980},
journal={BIT Numerical Mathematics},
volume={20},
number={2},
title={An improved {Monte Carlo} factorization algorithm},
url={https://doi.org/10.1007/BF01933190},
publisher={Kluwer Academic Publishers},
author={Brent, Richard P.},
pages={176-184},
language={English}
}

% Code: https://searchcode.com/codesearch/view/5110114/
@inproceedings{DBLP:conf/vmcai/Leino12,
  author    = {K. Rustan M. Leino},
  title     = {Automating Induction with an {SMT} Solver},
  booktitle = {{VMCAI} 2012},
  pages     = {315--331},
  year      = {2012},
  url       = {https://doi.org/10.1007/978-3-642-27940-9_21}
}

@Misc{Filliatre:2007,
  author =    "Filliâtre, Jean-Christophe",
  title =     "Tortoise and hare algorithm",
  year =      2007,
  url = "http://www.lix.polytechnique.fr/coq/pylons/contribs/files/TortoiseHareAlgorithm/v8.4/TortoiseHareAlgorithm.TortoiseHareAlgorithm.html"
}

@Book{Harper:PiSML:2011,
  author =    {Robert Harper},
  title =        "Programming in {Standard ML}",
  publisher =    "Unpublished",
  year =         2011,
  url = "http://www.cs.cmu.edu/~rwh/smlbook/"
}

@article{DBLP:journals/ipl/Nivasch04,
  author    = {Gabriel Nivasch},
  title     = {Cycle detection using a stack},
  journal   = {Inf. Process. Lett.},
  volume    = {90},
  number    = {3},
  pages     = {135--140},
  year      = {2004},
  url       = {http://www.gabrielnivasch.org/fun/cycle-detection},
  timestamp = {Tue, 06 Jul 2004 13:32:57 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/ipl/Nivasch04},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@article{DBLP:journals/jam/WangZ12,
  author    = {Ping Wang and
               Fangguo Zhang},
  title     = {An Efficient Collision Detection Method for Computing Discrete Logarithms
               with {Pollard}'s rho},
  journal   = {J. Applied Mathematics},
  volume    = {2012},
  year      = {2012},
  url       = {https://doi.org/10.1155/2012/635909},
  timestamp = {Mon, 27 Feb 2012 09:26:07 +0100},
  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/jam/WangZ12},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
