Inferring expected runtimes of probabilistic integer programs using expected sizes
From MaRDI portal
Publication:2044203
DOI10.1007/978-3-030-72016-2_14zbMath1467.68066arXiv2010.06367OpenAlexW3143328764MaRDI QIDQ2044203
Marcel Hark, Jürgen Giesl, Fabian Meyer
Publication date: 4 August 2021
Full work available at URL: https://arxiv.org/abs/2010.06367
Analysis of algorithms and problem complexity (68Q25) Integer programming (90C10) Stochastic programming (90C15)
Related Items
Learning probabilistic termination proofs ⋮ Latticed \(k\)-induction with an application to probabilistic programs ⋮ The probabilistic termination tool amber ⋮ Inferring expected runtimes of probabilistic integer programs using expected sizes ⋮ KoAT
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Cost analysis of object-oriented bytecode programs
- Semantics of probabilistic programs
- On probabilistic term rewriting
- Inferring expected runtimes of probabilistic integer programs using expected sizes
- Automated resource analysis with Coq proof objects
- On multiphase-linear ranking functions
- Automated termination analysis of polynomial probabilistic programs
- Termination of nondeterministic probabilistic programs
- Computing expected runtimes for constant probability programs
- Analyzing innermost runtime complexity of term rewriting by dependency pairs
- Analyzing program termination and complexity automatically with \textsf{AProVE}
- Complexity and resource bound analysis of imperative programs using difference constraints
- Closed-form upper bounds in static cost analysis
- Resource Analysis of Complex Programs with Cost Equations
- Probabilistic Termination
- Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs
- On the Inference of Resource Usage Upper and Lower Bounds
- A Combination Framework for Complexity
- Proving Positive Almost Sure Termination Under Strategies
- A Transformation System for Developing Recursive Programs
- Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms
- Reasoning about Recursive Probabilistic Programs
- Abstraction, Refinement and Proof for Probabilistic Systems
- Multi-dimensional Rankings, Program Termination, and Complexity Bounds of Flowchart Programs
- Resource Analysis driven by (Conditional) Termination Proofs
- Expected Runtime Analyis by Program Verification
- Termination Analysis of Probabilistic Programs with Martingales
- Stochastic invariants for probabilistic termination
- Towards automatic resource bound analysis for OCaml
- Complexity verification using guided theorem enumeration
- Type-based amortized resource analysis with integers and arrays
- Multivariate amortized resource analysis
- Static Analysis
- Ranking Functions for Linear-Constraint Loops
- Term Rewriting and Applications
- Computer Aided Verification
- Verification, Model Checking, and Abstract Interpretation
- New approaches for almost-sure termination of probabilistic programs
