Certified abstract cost analysis
From MaRDI portal
Publication:2044174
DOI10.1007/978-3-030-71500-7_2zbMath1467.68034OpenAlexW3139128041MaRDI QIDQ2044174
Elvira Albert, Dominic Steinhöfel, Alicia Merayo, Reiner Hähnle
Publication date: 4 August 2021
Full work available at URL: https://doi.org/10.1007/978-3-030-71500-7_2
Cites Work
- Unnamed Item
- Magic-sets for localised analysis of Java bytecode
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- A new look at the automatic synthesis of linear ranking functions
- Cost analysis of object-oriented bytecode programs
- Automatic verification of Java programs with dynamic frames
- Isabelle/HOL. A proof assistant for higher-order logic
- Deductive software verification: from pen-and-paper proofs to industrial tools
- Complexity and resource bound analysis of imperative programs using difference constraints
- Resource Analysis of Complex Programs with Cost Equations
- Ensuring the Correctness of Lightweight Tactics for JavaCard Dynamic Logic
- ABC: Algebraic Bound Computation for Loops
- Dafny: An Automatic Program Verifier for Functional Correctness
- Proving Termination of Programs Automatically with AProVE
- Amortized Resource Analysis with Polynomial Potential
- Inference Rules for Proving the Equivalence of Recursive Procedures
- Mechanical program analysis
- Symbolic execution and program testing
- Resource bound certification
- SPEED
- An Improved Tight Closure Algorithm for Integer Octagonal Constraints
