Tight polynomial bounds for Loop programs in polynomial space

Ben-Amram, Amir M. and Hamilton, GeoffORCID: 0000-0001-5954-6444
(2019)
Tight polynomial bounds for Loop programs in polynomial space.
In: International Conference on Foundations of Software Science and Computation Structures, 8-11 Apr 2019, Prague, Czech Republic.
ISBN 978-3-030-17126-1

We consider the following problem: given a program, find tight asymptotic
bounds on the values of some variables at the end of the computation (or at any given
program point) in terms of its input values. We focus on the case of polynomially-bounded
variables, and on a weak programming language for which we have recently shown that
tight bounds for polynomially-bounded variables are computable. These bounds are sets
of multivariate polynomials. While their computability has been settled, the complexity
of this program-analysis problem remained open. In this paper, we show the problem to
be PSPACE-complete. The main contribution is a new, space-efficient analysis algorithm.
This algorithm is obtained in a few steps. First, we develop an algorithm for univariate
bounds, a sub-problem which is already PSPACE-hard. Then, a decision procedure for
multivariate bounds is achieved by reducing this problem to the univariate case; this
reduction is orthogonal to the solution of the univariate problem and uses observations on
the geometry of a set of vectors that represent multivariate bounds. Finally, we transform
the univariate-bound algorithm to produce multivariate bounds.

Item Type:

Conference or Workshop Item (Paper)

Event Type:

Conference

Refereed:

Yes

Additional Information:

The European Joint Conferences on Theory and Practice of Software.

FoSSaCS 2019: Foundations of Software Science and Computation Structures. Lecture Notes in Computer Science (LNCS)
11425.
Springer. ISBN 978-3-030-17126-1