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