Control-Flow Refinement for Complexity Analysis of Probabilistic Programs in KoAT
Nils Lommen, \'El\'eanore Meyer, J\"urgen Giesl
TL;DR
This paper extends control-flow refinement (CFR) techniques to probabilistic programs, enhancing the complexity analysis capabilities of the KoAT tool with proven soundness and practical implementation.
Contribution
It introduces a sound extension of CFR to probabilistic programs and integrates it into KoAT for improved complexity analysis.
Findings
CFR can be effectively extended to probabilistic programs.
The implementation in KoAT demonstrates practical benefits.
The approach is sound for complexity analysis of probabilistic programs.
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFault Detection and Control Systems · Advanced Control Systems Optimization · Formal Methods in Verification