PURRS: Towards Computer Algebra Support for Fully Automatic Worst-Case Complexity Analysis
Roberto Bagnara, Andrea Pescetti, Alessandro Zaccagnini, Enea, Zaffanella (University of Parma)

TL;DR
This paper introduces PURRS, a system designed to provide comprehensive computer algebra support for fully automatic worst-case complexity analysis, especially handling recurrence relations more effectively.
Contribution
The paper presents PURRS, a new system that enhances computer algebra capabilities to better support automatic worst-case complexity analysis of programs.
Findings
PURRS effectively solves a broader class of recurrence relations.
It reduces the need for user intervention in complexity analysis.
Demonstrated on real-time embedded system programs.
Abstract
Fully automatic worst-case complexity analysis has a number of applications in computer-assisted program manipulation. A classical and powerful approach to complexity analysis consists in formally deriving, from the program syntax, a set of constraints expressing bounds on the resources required by the program, which are then solved, possibly applying safe approximations. In several interesting cases, these constraints take the form of recurrence relations. While techniques for solving recurrences are known and implemented in several computer algebra systems, these do not completely fulfill the needs of fully automatic complexity analysis: they only deal with a somewhat restricted class of recurrence relations, or sometimes require user intervention, or they are restricted to the computation of exact solutions that are often so complex to be unmanageable, and thus useless in practice.…
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
TopicsEmbedded Systems Design Techniques · Real-Time Systems Scheduling · Formal Methods in Verification
