Control-flow refinement for complexity analysis of probabilistic programs in \textsf{KoAT} (short paper)

DOI10.1007/978-3-031-63498-7_14MaRDI QIDQ7034865zbMATH OpenFDO

Authors Nils Lommen, Éléanore Meyer, Jürgen Giesl

Publication date 31 January 2025

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-63498-7_14

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• A combination framework for complexity
• Analyzing innermost runtime complexity of term rewriting by dependency pairs
• Automated Expected Amortised Cost Analysis of Probabilistic Data Structures
• Automatic complexity analysis of integer programs via triangular weakly non-linear loops
• Automatic Inference of Upper Bounds for Recurrence Relations in Cost Analysis
• Complexity analysis for \textbf{Java} with \textsf{AProVE}
• Complexity and resource bound analysis of imperative programs using difference constraints
• Control-flow refinement by partial evaluation, and its application to termination and cost analysis
• Cost analysis of object-oriented bytecode programs
• Expected Runtime Analyis by Program Verification
• From Jinja bytecode to term rewriting: a complexity reflecting transformation
• Inferring expected runtimes of probabilistic integer programs using expected sizes
• Multi-dimensional rankings, program termination, and complexity bounds of flowchart programs
• Resource analysis driven by (conditional) termination proofs
• Targeting Completeness: Using Closed Forms for Size Bounds of Integer Programs
• Tools and algorithms for the construction and analysis of systems. 25 years of TACAS: TOOLympics, held as part of ETAPS 2019, Prague, Czech Republic, April 6--11, 2019. Proceedings. Part III
• Towards automatic resource bound analysis for OCaml
• Weakest precondition reasoning for expected runtimes of randomized algorithms

Cited in

(3)

• Data-driven runtime complexity analysis
• From innermost to full probabilistic term rewriting: almost-sure termination, complexity, and modularity
• Targeting completeness: automated complexity analysis of integer programs

This page was built for publication: Control-flow refinement for complexity analysis of probabilistic programs in \textsf{KoAT} (short paper)

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q7034865)