scientific article; zbMATH DE number 7649967
From MaRDI portal
Publication:5875426
Cites work
- A Coq library for internal verification of running-times
- A fistful of dollars: formalizing asymptotic complexity claims via deductive program verification
- A mechanically verified incremental garbage collector
- A new approach to incremental cycle detection and related problems
- A semi-automatic proof of strong connectivity
- Amortised resource analysis with separation logic
- Amortized complexity verified
- Amortized Computational Complexity
- An axiomatic basis for computer programming
- Analyzing program termination and complexity automatically with \textsf{AProVE}
- Automated resource analysis with Coq proof objects
- Characteristic formulae for the verification of imperative programs
- Complexity verification using guided theorem enumeration
- Contract-based resource verification for higher-order functions with memoization
- Cost analysis of object-oriented bytecode programs
- Formalization techniques for asymptotic reasoning in classical analysis
- Hoare logics for time bounds. A study in meta theory
- Iris from the ground up: a modular foundation for higher-order concurrent separation logic
- Lightweight semiformal time complexity analysis for purely functional data structures
- Mechanical program analysis
- Refinement to Imperative/HOL
- Separation logic and abstraction
- SPEED: precise and efficient static estimation of program computational complexity
- SPEED: Symbolic Complexity Bound Analysis
- Towards automatic resource bound analysis for OCaml
- Universe polymorphism in Coq
- Verified efficient implementation of Gabow's strongly connected component algorithm
- Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits
Cited in
(9)- Selectively-amortized resource bounding
- Automated verification of the parallel Bellman-Ford algorithm
- For a few dollars more. Verified fine-grained algorithm analysis down to LLVM
- scientific article; zbMATH DE number 7439738 (Why is no real title available?)
- scientific article; zbMATH DE number 7649969 (Why is no real title available?)
- Incremental dead state detection in logarithmic time
- Correct and complete type checking and certified erasure for \textsc{Coq}, in \textsc{Coq}
- Touring the MetaCoq project
- A mechanically verified garbage collector for OCaml
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5875426)
