pymwp: A Tool for Guaranteeing Complexity Bounds for C Programs

TL;DR

pymwp is a static analysis tool for C programs that guarantees polynomial complexity bounds using an improved mwp-flow analysis, offering compositionality and applicability to non-terminating programs, addressing previous computational and feedback limitations.

Contribution

The paper introduces pymwp, a tool that applies an enhanced mwp-flow analysis to automatically verify polynomial resource bounds in C programs.

Findings

Successfully analyzes resource usage in C programs.

Handles non-terminating programs with polynomial bounds.

Provides automated complexity guarantees.

Abstract

Complexity analysis offers assurance of program's runtime behavior, but large classes of programs remain unanalyzable by existing automated techniques.The mwp-flow analysis sidesteps many difficulties shared by existing approaches, and offers interesting features, such as compositionality, multivariate bounds, and applicability to non-terminating programs.It analyzes resource usage and determines if a program's variables growth rates are no more than polynomially related to their inputs sizes.This sound calculus, however, is computationally expensive to manipulate, and provides no feedback if the program does not have polynomial bounds.Those two defaults were addressed in a previous work, and prepared for the tool we present here: pymwp, a static complexity analyzer for C programs based on our improved mwp-flow analysis.