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
Cost analysis of object-oriented bytecode programs, Theoretical Computer Science, vol.413, issue.1, pp.142-159, 2012. ,
Amortised resource analysis with separation logic, Logical Methods in Computer Science, vol.7, issue.2, p.17, 2011. ,
A new approach to incremental cycle detection and related problems, ACM Transactions on Algorithms, vol.12, issue.2, 2016. ,
Automated resource analysis with Coq proof objects, Computer Aided Verification (CAV), vol.10427, pp.64-85, 2017. ,
Characteristic formulae for the verification of imperative programs, 2013. ,
The CFML tool and library, 2019. ,
Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits, 2017. ,
Formal proofs of Tarjan's algorithm in Why3, Coq, and Isabelle. Manuscript, 2018. ,
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
Lightweight semiformal time complexity analysis for purely functional data structures, Principles of Programming Languages (POPL), 2008. ,
A fully verified executable LTL model checker, Computer Aided Verification (CAV), vol.8044, pp.463-478, 2013. ,
URL : https://hal.archives-ouvertes.fr/hal-01226469
Analyzing program termination and complexity automatically with AProVE, Journal of Automated Reasoning, vol.58, issue.1, pp.3-31, 2017. ,
SPEED: symbolic complexity bound analysis, Computer Aided Verification (CAV), vol.5643, pp.51-62, 2009. ,
SPEED: precise and efficient static estimation of program computational complexity, Principles of Programming Languages (POPL), pp.127-139, 2009. ,
Dune pull request #1955, 2019. ,
A fistful of dollars: Formalizing asymptotic complexity claims via deductive program verification, European Symposium on Programming, vol.10801, pp.533-560, 2018. ,
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. ,
An axiomatic basis for computer programming, Communications of the ACM, vol.12, issue.10, pp.576-580, 1969. ,
Towards automatic resource bound analysis for OCaml, Principles of Programming Languages (POPL), pp.359-373, 2017. ,
Statically-informed dynamic analysis tools to detect algorithmic complexity vulnerabilities, Source Code Analysis and Manipulation (SCAM), pp.79-84, 2016. ,
Computer science: The emergence of a discipline, Communications of the ACM, vol.30, issue.3, pp.198-202, 1987. ,
, Coq pull request #89, 2015.
Iris from the ground up: A modular foundation for higher-order concurrent separation logic, Journal of Functional Programming, vol.28, issue.20, 2018. ,
URL : https://hal.archives-ouvertes.fr/hal-01945446
Verified efficient implementation of Gabow's strongly connected component algorithm, Interactive Theorem Proving (ITP), vol.8558, pp.325-340, 2014. ,
Refinement to Imperative/HOL, Interactive Theorem Proving (ITP), vol.9236, pp.253-269, 2015. ,
A framework for verifying depth-first search algorithms, Certified Programs and Proofs (CPP), pp.137-146, 2015. ,
PerfFuzz: Automatically generating pathological inputs, International Symposium on Software Testing and Analysis (ISSTA), pp.254-265, 2018. ,
Contract-based resource verification for higher-order functions with memoization, Principles of Programming Languages (POPL), pp.330-343, 2017. ,
A Coq library for internal verification of running-times, Functional and Logic Programming, vol.9613, pp.144-162, 2016. ,
Efficient flow profiling for detecting performance bugs, International Symposium on Software Testing and Analysis (ISSTA), pp.413-424, 2016. ,
Time credits and time receipts in Iris, European Symposium on Programming, vol.11423, pp.1-27, 2019. ,
Amortized complexity verified, Interactive Theorem Proving (ITP), vol.9236, pp.310-324, 2015. ,
Static detection of asymptotic performance bugs in collection traversals, Programming Language Design and Implementation (PLDI), pp.369-378, 2015. ,
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
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. ,
Universe polymorphism in Coq, Interactive Theorem Proving (ITP), vol.8558, pp.499-514 ,
URL : https://hal.archives-ouvertes.fr/hal-00974721
, , 2014.
Complexity verification using guided theorem enumeration, Principles of Programming Languages (POPL), pp.639-652, 2017. ,
Dune: A composable build system, 2018. ,
, 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. ,
, The Coq development team. The Coq Proof Assistant, 2019.
Synthesizing programs that expose performance bottlenecks, Code Generation and Optimization (CGO), pp.314-326, 2018. ,
A machine-checked proof of the average-case complexity of Quicksort in Coq, Types for Proofs and Programs, vol.5497, pp.256-271, 2008. ,
Mechanical program analysis, Communications of the ACM, vol.18, issue.9, pp.528-539, 1975. ,