2023/07/13 by Nils Lommen, Lommen, Nils, Jürgen Giesl +1 · 2 citations
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Software Engineering Research #Software Testing and Debugging Techniques
paper · pdf · doi:10.48550/arxiv.2307.06921
openalex publication_date 2023/07/13 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We present a new procedure to infer size bounds for integer programs automatically. Size bounds are important for the deduction of bounds on the runtime complexity or in general, for the resource analysis of programs. We show that our technique is complete (i.e., it always computes finite size bounds) for a subclass of loops, possibly with non-linear arithmetic. Moreover, we present a novel approach to combine and integrate this complete technique into an incomplete approach to infer size and runtime bounds of general integer programs. We prove completeness of our integration for an important subclass of integer programs. We implemented our new algorithm in the automated complexity analysis tool KoAT to evaluate its power, in particular on programs with non-linear arithmetic.