Control-Flow Refinement for Complexity Analysis of Probabilistic Programs in KoAT

2024/02/06 by Nils Lommen, Lommen, Nils, Éléanore Meyer +3 · 2 citations
Computer Science · Engineering · #Advanced Control Systems Optimization #FOS: Computer and information sciences #Fault Detection and Control Systems #Formal Methods in Verification #Logic in Computer Science (cs.LO)

paper · pdf · doi:10.48550/arxiv.2402.03891

openalex publication_date 2024/02/06 · openalex created_date 2024/02/08 · openalex updated_date 2026/07/28

Abstract

Recently, we showed how to use control-flow refinement (CFR) to improve automatic complexity analysis of integer programs. While up to now CFR was limited to classical programs, in this paper we extend CFR to probabilistic programs and show its soundness for complexity analysis. To demonstrate its benefits, we implemented our new CFR technique in our complexity analysis tool KoAT.

Cited by

• Modular Automatic Complexity Analysis of Recursive Integer Programs
• Dependency Pairs for Expected Innermost Runtime Complexity and Strong Almost-Sure Termination of Probabilistic Term Rewriting

Related

• Improving Automatic Complexity Analysis of Integer Programs
• Structural Abstraction and Refinement for Probabilistic Programs
• Modular Runtime Complexity Analysis of Probabilistic While Programs
• The Complexity of Synthesis from Probabilistic Components
• Program Analysis of Probabilistic Programs