pymwp: A Tool for Guaranteeing Complexity Bounds for C Programs
Cl\'ement Aubert, Thomas Rubiano (LIPN), Neea Rusch, Thomas Seiller, (LIPN, CNRS)

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.
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
TopicsSoftware Engineering Research · Software Reliability and Analysis Research · Formal Methods in Verification
