@article(Benzinger,
 author       = {Ralph Benzinger},
 year         = {2004},
 title        = {Automated Higher-order Complexity Analysis},
 journal      = {Theoretical Computer Science},
 volume       = {318},
 number       = {1-2},
 pages        = {79--103},
 doi          = {10.1016/j.tcs.2003.10.022},
)
@article(BevierHuntMooreYoung89,
 author       = {William R. Bevier and {Hunt, Jr.}, Warren and J Strother Moore and William Young},
 year         = {1989},
 title        = {An Approach to Systems Verification},
 journal      = {Journal of Automated Reasoning},
 volume       = {5},
 number       = {4},
 pages        = {411--428},
 doi          = {10.1007/BF00243131},
)
@article(BoyerMoore77,
 author       = {Robert S. Boyer and J Strother Moore},
 year         = {1977},
 title        = {A Fast String Searching Algorithm},
 journal      = {Communications of the ACM},
 volume       = {20},
 number       = {10},
 pages        = {762--772},
 doi          = {10.1145/359842.359859},
)
@incollection(BoyerMoore91,
 author       = {Robert S. Boyer and J Strother Moore},
 year         = {1991},
 title        = {MJRTY: A Fast Majority Vote Algorithm},
 editor       = {Robert S. Boyer},
 booktitle    = {Automated Reasoning: Essays in Honor of Woody Bledsoe},
 publisher    = {Kluwer Academic Publishers},
 address      = {Dordrecht, The Netherlands},
 pages        = {105--117},
 doi          = {10.1007/978-94-011-3488-0\_5},
)
@incollection(BoyerMoore96,
 author       = {Robert S. Boyer and J Strother Moore},
 year         = {1996},
 title        = {Mechanized Formal Reasoning about Programs and Computing Machines},
 editor       = {R. Veroff},
 booktitle    = {Automated Reasoning and Its Applications: Essays in Honor of Larry Wos},
 publisher    = {MIT Press},
 address      = {Boston},
 pages        = {141--176},
 doi          = {10.1.1.27.8666},
)
@inproceedings(BrockKaufmannMoore96,
 author       = {Bishop Brock and Matt Kaufmann and J Strother Moore},
 year         = {1996},
 title        = {ACL2 Theorems about Commercial Microprocessors},
 booktitle    = {Formal Methods in Computer-Aided Design (FMCAD'96)},
 publisher    = {Springer-Verlag},
 pages        = {275--293},
 doi          = {10.1007/BFb0031816},
)
@inproceedings(Carbonneaux,
 author       = {Q. Carbonneaux and J. Hoffmann and T.W. Reps and Z. Shao},
 year         = {2017},
 title        = {Automated Resource Analysis with {Coq} Proof Objects},
 booktitle    = {Computer Aided Verification (CAV 2017)},
 publisher    = {Springer-Verlag},
 pages        = {64--85},
 doi          = {10.1007/978-3-319-22102-1\_9},
)
@misc(Chargueraud,
 author       = {A. Chargu\'eraud},
 year         = {2019},
 title        = {The CFML Tool and Library},
 howpublished = {\url{https://www.chargueraud.org/softs/cfml/}},
)
@article(ChargueraudPottier,
 author       = {A. Chargu\'eraud and F. Pottier},
 year         = {2019},
 title        = {Verifying the Correctness and Amortized Complexity of a Union-Find Implementation in Separation Logic with Time Credits},
 journal      = {Journal of Automated Reasoning},
 volume       = {62},
 number       = {3},
 pages        = {331--365},
 doi          = {10.1007/s10817-017-9431-7},
)
@inproceedings(CowlesGreveYoung,
 author       = {John Cowles and David Greve and William Young},
 year         = {2007},
 title        = {The While Language Challenge: First Progress},
 booktitle    = {Proceedings of the Seventh International Workshop on the ACL2 Theorem Prover and its Applications},
)
@article(Flajolet,
 author       = {Philippe Flajolet and Bruno Salvy and Paul Zimmermann},
 year         = {1991},
 title        = {Automatic Average-Case Analysis of Algorithms},
 journal      = {Theoretical Computer Science},
 volume       = {79},
 pages        = {37--109},
 doi          = {10.1016/0304-3975(91)90145-R},
)
@incollection(Gueneau18,
 author       = {A. Gu\'eneau and A. Chargu\'eraud and F. Pottier},
 year         = {2018},
 title        = {A Fistful of Dollars: Formalizing Asymptotic Complexity Claims via Deductive Program Verification},
 editor       = {A. Ahmed},
 booktitle    = {Programming Languages and Systems (ESOP 2018)},
 publisher    = {Springer},
 address      = {New York},
 doi          = {10.1007/978-3-319-89884-1\_19},
)
@phdthesis(Gueneau20,
 author       = {Arma\"el Gu\'eneau},
 year         = {2020},
 title        = {Mechanical Verification of the Correctness and Asymptotic Complexity of Programs: The Right Answer at the Right Time},
 school       = {University of Paris},
)
@article(HartmanisStearns,
 author       = {Juris Hartmanis and Richard E. Stearns},
 year         = {1965},
 title        = {On the computational complexity of algorithms},
 journal      = {Transactions of the American Mathematical Society},
 volume       = {117},
 pages        = {285--306},
 doi          = {10.1090/S0002-9947-1965-0170805-7},
)
@article(HickeyCohen,
 author       = {T. Hickey and J. Cohen},
 year         = {1988},
 title        = {Automated Program Analysis},
 journal      = {Journal of the ACM},
 volume       = {35},
 number       = {1},
 pages        = {185--220},
 doi          = {10.1145/99370.99381},
)
@inproceedings(HofmannJost,
 author       = {M. Hofmann and S. Jost},
 year         = {2003},
 title        = {Static Prediction of Heap Space Usage for First-Order Functional Programs},
 booktitle    = {Proceedings of the 30th ACM Symposium on Principles of Programming Languages},
 publisher    = {ACM},
 pages        = {185--197},
 doi          = {10.1.1.175.6871},
)
@inbook(HuntKaufmannMooreSlobodova17,
 author       = {Warren Hunt and Matt Kaufmann and J Strother Moore and Anna Slobodova},
 year         = {2017},
 title        = {Verified Trustworthy Software Systems},
 chapter      = {Industrial Hardware and Software Verification with ACL2},
 series       = {Philosophical Transactions A, vol. 374},
 publisher    = {Royal Society Publishing},
 doi          = {10.1098/rsta.2015.0399},
)
@inproceedings(Iqbal19,
 author       = {N. Iqbal and O. Hasan and U. Siddique and F. Awwad},
 year         = {2019},
 title        = {Formalization of Asymptotic Notations in HOL-4},
 booktitle    = {4th International Conference on Computer and Commumication Systems},
 publisher    = {IEEE},
 pages        = {383--387},
 doi          = {10.1007/978-3-030-78409-6\_5},
)
@article(LeMetayer,
 author       = {{Le M\'etayer}, Daniel},
 year         = {1988},
 title        = {ACE: an automatic complexity evaluator},
 journal      = {ACM Transactions on Programming Languages and Systems},
 volume       = {10},
 number       = {2},
 pages        = {248--266},
 doi          = {10.1145/42190.42347},
)
@inbook(Moore99,
 author       = {J Strother Moore},
 year         = {1999},
 title        = {Correct System Design---Recent Insights and Advances},
 chapter      = {Proving Theorems about Java-like Byte Code},
 pages        = {139--162},
 series       = {LNCS: State of the Art Survey, vol. 1710},
 publisher    = {Springer-Verlag},
 doi          = {10.1007/3-540-48092-7\_7},
)
@article(NipkowBrinkop,
 author       = {T. Nipkow and H. Brinkop},
 year         = {2019},
 title        = {Amortized Complexity Verified},
 journal      = {Journal of Automated Reasoning},
 volume       = {62},
 pages        = {367--391},
 doi          = {10.1007/s10817-018-9459-3},
)
@incollection(RayMoore,
 author       = {S. Ray and J S. Moore},
 year         = {2004},
 title        = {Proof Styles in Operational Semantics},
 editor       = {A. J. Hu and A. K. Martin},
 booktitle    = {Proceedings of the 5th International Conference on Formal Methods in Computer-aided Design (FMCAD 2004): LNCS 3312},
 publisher    = {Springer-Verlag},
 address      = {New York},
 pages        = {67--81},
 doi          = {10.1007/978-3-540-30494-4\_6},
)
@book(Sipser,
 author       = {Michael Sipser},
 year         = {2006},
 title        = {Introduction to the Theory of Computation (Second Edition)},
 publisher    = {Thompson Course Technology},
 address      = {Boston},
)
@article(Wegbreit,
 author       = {Ben Wegbreit},
 year         = {1975},
 title        = {Mechanical Program Analysis},
 journal      = {Communications of the ACM},
 volume       = {18},
 number       = {9},
 pages        = {528--539},
 doi          = {10.1145/361002.361016},
)