Certified complexity (CerCo). In Foundational and Practical Aspects of Resource Analysis, Lecture Notes in Computer Science, vol.8552, pp.1-18, 2014. ,
Cost analysis of object-oriented bytecode programs, Theoretical Computer Science, vol.413, issue.1, pp.142-159, 2012. ,
Certifying and reasoning on cost annotations in C programs, Formal Methods for Industrial Critical Systems, vol.7437, pp.32-46, 2012. ,
URL : https://hal.archives-ouvertes.fr/hal-00702665
On the solution of linear recurrence equations, Comp. Opt. and Appl, vol.10, issue.2, pp.195-210, 1998. ,
, Deductive Software Verification -The KeY Book -From Theory to Practice, Lecture Notes in Computer Science, vol.10001, 2016.
On the limits of the classical approach to cost analysis, Static Analysis, pp.405-421, 2012. ,
Formalization techniques for asymptotic reasoning in classical analysis, Journal of Formalized Reasoning, vol.11, issue.1, pp.43-76, 2018. ,
URL : https://hal.archives-ouvertes.fr/hal-01719918
Formalizing O notation in Isabelle/HOL, International Joint Conference on Automated Reasoning, vol.3097, pp.357-371, 2004. ,
Automating sized-type inference for complexity analysis, Proc. ACM Program. Lang, vol.1, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01639200
Analysing the complexity of functional programs: Higher-order meets first-order, Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, pp.152-164, 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-01231809
A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses, CPP -Certified Programs and Proofs -First International Conference -2011, vol.7086, pp.135-150, 2011. ,
A combination framework for complexity, 24th International Conference on Rewriting Techniques and Applications, RTA 2013, pp.55-70, 2013. ,
Trustworthy Graph Algorithms (Invited Talk), 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019), vol.138, 2019. ,
Certifying and reasoning on cost annotations of functional programs, Foundational and Practical Aspects of Resource Analysis, vol.7177, pp.72-89, 2011. ,
Amortised resource analysis with separation logic, Logical Methods in Computer Science, vol.7, issue.2, p.17, 2011. ,
Alternating runtime and size complexity analysis of integer programs, Tools and Algorithms for the Construction and Analysis of Systems, pp.140-155, 2014. ,
Automated higher-order complexity analysis, Theor. Comput. Sci, vol.318, issue.1-2, pp.79-103, 2004. ,
A new approach to incremental cycle detection and related problems, ACM Transactions on Algorithms, vol.12, issue.2, 2016. ,
Iron: Managing obligations in higher-order concurrent separation logic, Proc. ACM Program. Lang, vol.3, 2019. ,
Abc: Algebraic bound computation for loops, Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), pp.103-118, 2010. ,
A general method for solving divide-and-conquer recurrences, SIGACT News, vol.12, issue.3, pp.36-44, 1980. ,
Imperative functional programming with Isabelle/HOL, Theorem Proving in Higher Order Logics (TPHOLs), vol.5170, pp.134-149, 2008. ,
Coquelicot: A userfriendly library of real analysis for Coq, Mathematics in Computer Science, vol.9, issue.1, pp.41-62, 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-00860648
, General Topology, 1995.
Modular and Certified Resource-Bound Analyses, 2018. ,
Formal proofs of Tarjan's algorithm in Why3, Coq, and Isabelle. Manuscript, 2018. ,
The TLC coq library ,
Characteristic Formulae for Mechanized Program Verification, 2010. ,
The optimal fixed point combinator, Interactive Theorem Proving (ITP), vol.6172, pp.195-210, 2010. ,
Characteristic formulae for the verification of imperative programs, 2013. ,
The cfml2 framework, 2019. ,
The CFML tool and library, 2019. ,
End-to-end verification of stack-space bounds for C programs, Programming Language Design and Implementation (PLDI), pp.270-281, 2014. ,
Automated resource analysis with Coq proof objects, Computer Aided Verification (CAV), vol.10427, pp.64-85 ,
, , 2017.
Compositional certified resource bounds, Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '15, pp.467-478, 2015. ,
A semi-automatic proof of strong connectivity, Verified Software: Theories, Tools and Experiments, vol.10712, pp.49-65, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01632947
, , 2009.
Formalized algebraic numbers: construction and first-order theory, 2012. ,
URL : https://hal.archives-ouvertes.fr/pastel-00780446
Theorem proving in arithmetic without multiplication, Machine Intelligence 7, pp.91-99, 1972. ,
Temporary read-only permissions for separation logic, European Symposium on Programming, vol.10201, pp.260-286, 2017. ,
Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits, Journal of Automated Reasoning, 2017. ,
Effective DoS attacks against web application platforms ,
Resource bound certification, Principles of Programming Languages (POPL), pp.184-198, 2000. ,
Lightweight semiformal time complexity analysis for purely functional data structures, Principles of Programming Languages (POPL), 2008. ,
Denotational cost semantics for functional languages with inductive types, Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, pp.140-151, 2015. ,
A static cost analysis for a higher-order language, Programming Languages Meets Program Verification (PLPV), pp.25-34, 2013. ,
Proving divide and conquer complexities in Isabelle/HOL, Journal of Automated Reasoning, vol.58, issue.4, pp.483-508, 2017. ,
Verified solving and asymptotics of linear recurrences, Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, pp.27-37, 2019. ,
A Certifying Extraction with Time Bounds from Coq to Call-By-Value Lambda Calculus, 10th International Conference on Interactive Theorem Proving (ITP 2019), vol.141, pp.1-17, 2019. ,
Functors for proofs and programs, European Symposium on Programming, vol.2986, pp.370-384, 2004. ,
Resource analysis of complex programs with cost equations, Programming Languages and Systems, pp.275-295, 2014. ,
Why3-where programs meet provers, European Symposium on Programming, vol.7792, pp.125-128, 2013. ,
A fistful of dollars: Formalizing asymptotic complexity claims via deductive program verification, European Symposium on Programming, vol.10801, pp.533-560, 2018. ,
The verified incremental cycle detection library, 2019. ,
SPEED: precise and efficient static estimation of program computational complexity, Principles of Programming Languages (POPL), pp.127-139, 2009. ,
Verified characteristic formulae for CakeML, European Symposium on Programming, vol.10201, pp.584-610, 2017. ,
The minicooper library, 2018. ,
, Armaël Guéneau. Coq issue #6723
, Armaël Guéneau. Coq issue #6726
Manual of the procrastination library, 2018. ,
The bigO library, 2018. ,
The procrastination library, 2018. ,
Dune pull request #1955, 2019. ,
SPEED: symbolic complexity bound analysis, Computer Aided Verification (CAV), vol.5643, pp.51-62, 2009. ,
Multivariate amortized resource analysis, ACM Transactions on Programming Languages and Systems, vol.34, issue.3, 2012. ,
Resource aware ML, Computer Aided Verification (CAV), vol.7358, pp.781-786, 2012. ,
Handbook of Practical Logic and Automated Reasoning, 2009. ,
Towards automatic resource bound analysis for OCaml, Principles of Programming Languages (POPL), pp.359-373, 2017. ,
Amortized resource analysis with polynomial potential, European Symposium on Programming, vol.6012, pp.287-306, 2010. ,
Type classes and filters for mathematical analysis in isabelle/hol, Interactive Theorem Proving, pp.279-294, 2013. ,
Static prediction of heap space usage for first-order functional programs, Principles of Programming Languages (POPL), pp.185-197, 2003. ,
Refinement with Time -Refining the Run-Time of Algorithms in Isabelle/HOL, 10th International Conference on Interactive Theorem Proving (ITP 2019), vol.141, pp.1-20, 2019. ,
Amortised resource analysis and typed polynomial interpretations, Rewriting and Typed Lambda Calculi, pp.272-286, 2014. ,
Quantitative reasoning for proving lock-freedom, Logic in Computer Science (LICS), pp.124-133, 2013. ,
Hoare logics for time bounds: A study in meta theory, Tools and Algorithms for Construction and Analysis of Systems (TACAS), vol.10805, pp.155-171, 2018. ,
Linear types and non size-increasing polynomial time computation, Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, LICS '99, p.464, 1999. ,
Computer science: The emergence of a discipline, Communications of the ACM, vol.30, issue.3, pp.198-202, 1987. ,
On asymptotic notation with multiple variables, 2008. ,
Statically-informed dynamic analysis tools to detect algorithmic complexity vulnerabilities, Source Code Analysis and Manipulation (SCAM), pp.79-84, 2016. ,
Umair Siddique, and Falah Awwd. Formalization of asymptotic notations in hol4, IEEE 4th International Conference on Computer and Communication Systems (ICCCS), 2019. ,
Static determination of quantitative resource usage for higher-order programs, Principles of Programming Languages (POPL), pp.223-236, 2010. ,
Iris from the ground up: A modular foundation for higher-order concurrent separation logic, Journal of Functional Programming, vol.28, issue.20, 2018. ,
, Coq pull request #89, 2015.
Exponential automatic amortized resource analysis, 2019. ,
Asymptotic notation. Part I: theory, Journal of Formalized Mathematics, vol.11, 1999. ,
Decision procedures -An algorithmic point of view, 2008. ,
Interactive proofs in higherorder concurrent separation logic, Principles of Programming Languages (POPL, 2017. ,
Verified efficient implementation of Gabow's strongly connected component algorithm, Interactive Theorem Proving (ITP), vol.8558, pp.325-340, 2014. ,
Notes on better master theorems for divide-and-conquer recurrences, 1996. ,
Arrays and References in Resource Aware ML, 2nd International Conference on Formal Structures for Computation and Deduction, vol.84, pp.1-26, 2017. ,
A separation logic framework for Imperative HOL. Archive of Formal Proofs, 2012. ,
PerfFuzz: Automatically generating pathological inputs, International Symposium on Software Testing and Analysis (ISSTA), pp.254-265, 2018. ,
Formalizing the edmonds-karp algorithm. Archive of Formal Proofs, 2016. ,
A Coq library for internal verification of runningtimes, Functional and Logic Programming, vol.9613, pp.144-162, 2016. ,
Time credits and time receipts in Iris, European Symposium on Programming, vol.11423, pp.1-27 ,
, , 2019.
Contract-based resource verification for higher-order functions with memoization, Principles of Programming Languages (POPL), pp.330-343, 2017. ,
Efficient flow profiling for detecting performance bugs, International Symposium on Software Testing and Analysis (ISSTA), pp.413-424, 2016. ,
Viper: A verification infrastructure for permission-based reasoning, Dependable Software Systems Engineering, pp.104-125, 2017. ,
Amortized complexity verified, Journal of Automated Reasoning, vol.62, issue.3, pp.367-391, 2019. ,
Hoare Logic's for Run-time Analysis of Programs, 1984. ,
A hoare-like proof system for analysing the computation time of programs, Sci. Comput. Program, vol.9, issue.2, pp.107-136, 1987. ,
Amortized complexity verified, Interactive Theorem Proving (ITP), vol.9236, pp.310-324 ,
, , 2015.
Badger: Complexity analysis with fuzzing and symbolic execution, Proceedings of the 27th ACM SIGSOFT International Symposium on Software Testing and Analysis, pp.322-332, 2018. ,
Semantics with applications: an appetizer, 2007. ,
Static detection of asymptotic performance bugs in collection traversals, Programming Language Design and Implementation (PLDI), pp.369-378, 2015. ,
Purely Functional Data Structures, 1999. ,
Separation logic and abstraction, Principles of Programming Languages (POPL), pp.247-258, 2005. ,
Depth-first search and strong connectivity in Coq, Journées Françaises des Langages Applicatifs (JFLA), 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-01096354
The essence of monotonic state, Types in Language Design and Implementation (TLDI), 2011. ,
URL : https://hal.archives-ouvertes.fr/hal-01081193
Slowfuzz: Automated domain-independent detection of algorithmic complexity vulnerabilities, Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS '17, pp.2155-2168, 2017. ,
Monadic refinements for relational cost analysis, Proc. ACM Program. Lang, vol.2, p.32, 2018. ,
Separation logic: A logic for shared mutable data structures, Logic in Computer Science (LICS), pp.55-74, 2002. ,
A mechanically verified incremental garbage collector, Formal Aspects of Computing, vol.6, issue.4, pp.359-390, 1994. ,
First-class type classes, Theorem Proving in Higher Order Logics (TPHOL), pp.278-293, 2008. ,
URL : https://hal.archives-ouvertes.fr/inria-00628864
Universe polymorphism in Coq, Interactive Theorem Proving (ITP), vol.8558, pp.499-514, 2014. ,
URL : https://hal.archives-ouvertes.fr/hal-00974721
Dune: A composable build system, 2018. ,
Verifying higher-order programs with the dijkstra monad, Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '13, pp.387-398, 2013. ,
A simple and scalable static analysis for bound analysis and amortized complexity analysis, Computer Aided Verification, pp.745-761, 2014. ,
, Amortized computational complexity. SIAM Journal on Algebraic and Discrete Methods, vol.6, issue.2, pp.306-318, 1985.
Algorithmic design, Communications of the ACM, vol.30, issue.3, pp.204-212, 1987. ,
Simplifying Polynomial Expressions in a Proof Assistant, INRIA, 2005. ,
, The Coq development team. The Coq Manual, Miscellaneous extensions: Program Derivation, 2019.
, The Coq development team. The Coq Proof Assistant, 2019.
Synthesizing programs that expose performance bottlenecks, Code Generation and Optimization (CGO), pp.314-326, 2018. ,
Inferring cost equations for recursive, polymorphic and higher-order functional programs, Proceedings of the 15th International Conference on Implementation of Functional Languages, IFL'03, pp.86-101, 2004. ,
A machine-checked proof of the average-case complexity of Quicksort in Coq, Types for Proofs and Programs, vol.5497, pp.256-271, 2008. ,
Type System for Resource Bounds with Type-Preserving Compilation, 2018. ,
Singularity: Pattern fuzzing for worst case complexity, Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, pp.213-223, 2018. ,
The worst-case execution-time problemoverview of methods and survey of tools, Staschulat, and Per Stenström, vol.7, p.53, 2008. ,
Mechanical program analysis, Communications of the ACM, vol.18, issue.9, pp.528-539, 1975. ,
TiML: A functional language for practical complexity analysis with invariants, Proceedings of the ACM on Programming Languages, vol.1, 2017. ,
Bound analysis of imperative programs with the size-change abstraction, Static Analysis, pp.280-297, 2011. ,
Coq's prolog and application to defining semi-automatic tactics, Type Theory Based Tools (TTT, 2017. ,
Verifying asymptotic time complexity of imperative programs in Isabelle, International Joint Conference on Automated Reasoning, 2018. ,
Efficient verification of imperative programs using auto2, Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp.23-40, 2018. ,