scientific article; zbMATH DE number 7649967
From MaRDI portal
Publication:5875426
DOI10.4230/LIPIcs.ITP.2019.18MaRDI QIDQ5875426
François Pottier, Jacques-Henri Jourdan, Arthur Charguéraud, Armaël Guéneau
Publication date: 3 February 2023
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (4)
Selectively-amortized resource bounding ⋮ Automated verification of the parallel Bellman-Ford algorithm ⋮ Unnamed Item ⋮ For a few dollars more. Verified fine-grained algorithm analysis down to LLVM
Uses Software
Cites Work
- Unnamed Item
- Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits
- Cost analysis of object-oriented bytecode programs
- A mechanically verified incremental garbage collector
- A semi-automatic proof of strong connectivity
- Automated resource analysis with Coq proof objects
- A fistful of dollars: formalizing asymptotic complexity claims via deductive program verification
- Hoare logics for time bounds. A study in meta theory
- Analyzing program termination and complexity automatically with \textsf{AProVE}
- A Coq Library for Internal Verification of Running-Times
- Verified Efficient Implementation of Gabow’s Strongly Connected Component Algorithm
- Universe Polymorphism in Coq
- Refinement to Imperative/HOL
- Amortized Complexity Verified
- Lightweight semiformal time complexity analysis for purely functional data structures
- Amortised Resource Analysis with Separation Logic
- SPEED: Symbolic Complexity Bound Analysis
- Amortized Computational Complexity
- Mechanical program analysis
- Iris from the ground up: A modular foundation for higher-order concurrent separation logic
- A New Approach to Incremental Cycle Detection and Related Problems
- Characteristic formulae for the verification of imperative programs
- SPEED
- Separation logic and abstraction
- Contract-based resource verification for higher-order functions with memoization
- Towards automatic resource bound analysis for OCaml
- Complexity verification using guided theorem enumeration
- An axiomatic basis for computer programming
This page was built for publication:
