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

The authors present a novel control-flow refinement (CFR) technique that can be used to improve the automated complexity analysis of probabilistic integer programs. They prove the soundness of their CFR approach and demonstrate its benefits by implementing it in their complexity analysis tool KoAT.