Abstract is a tool to automatically infer complexity bounds and prove termination of (possibly recursive) integer programs. To this end, implements an alternating modular inference of upper runtime and size bounds for program parts. In particular, uses a portfolio of different techniques to analyze subprograms. The power of our approach is demonstrated by an extensive experimental evaluation.

Abstract There exist several approaches to infer runtime or resource bounds for integer programs automatically. In this paper, we study the subclass of periodic rational solvable loops (prs-loops) , where questions regarding the runtime and the size of variable values are decidable and where we can therefore obtain techniques that are “complete” for such subclasses. We show how to use these results for the complexity analysis of arbitrary general integer programs. To this end, we present a modular approach which computes local runtime and size bounds for subprograms which correspond to prs -loops. These local bounds are then lifted to global runtime and size bounds for the whole integer program. Furthermore, we introduce several techniques to transform larger programs into prs -loops to increase the scope of the approach. The power of the procedure is shown by our implementation in the complexity analysis tool .

Abstract To (dis)prove termination of programs, uses symbolic execution to transform the program’s code into an integer transition system (ITS). These ITSs are analyzed by our backend tools (for termination) and (for non-termination) which we integrated into our novel framework to replace previously used external backend tools. In this way, we benefit from the recent improvements in the backend tools and . The transformation steps in and the tools in the backend produce sub-proofs which are then combined automatically in order to generate a complete termination proof. If non-termination is proved, then a witness for a non-terminating path in the original program is returned.

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 .