Tight Polynomial Worst-Case Bounds for Loop Programs

by Dr. Goeff Hamilton

• When: Friday, 05/11/2021, between 1pm and 2pm EDT (5pm-6pm UTC)
• Where: Zoom; Outside guests please RSVP by emailing Harley Eades
• Stream/Recording: https://youtu.be/l8NT3ReVUu4

Abstract

One of the most important properties we would like to know about programs is their resource usage, i.e., the amount of resources (such as time, memory, etc.) required for their execution. However, it is undecidable whether or not a variable’s value in a Turing-complete language is polynomially bounded, let alone determining what those polynomial bounds are. It has previously been shown by Ben-Amram, Jones and Kristiansen, for a slightly weaker language that is not Turing-complete, that it is possible to decide whether or not a variable’s value is polynomially bounded. However, finding these polynomial bounds is a difficult problem: the polynomial-bound analysis problem. In this talk, we show how to solve the polynomial-bound analysis problem by finding tight symbolic bounds (up to constant factors) on the polynomially bounded variables of a program in the language of Ben-Amram, Jones and Kristiansen.