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.

Abstract In 2008, Ben-Amram, Jones and Kristiansen showed that for a simple programming language—representing non-deterministic imperative programs with bounded loops, and arithmetics limited to addition and multiplication—it is possible to decide precisely whether a program has certain growth-rate properties, in particular whether a computed value, or the program’s running time, has a polynomial growth rate. A natural and intriguing problem was to improve the precision of the information obtained. This paper shows how to obtain asymptotically-tight multivariate polynomial bounds for this class of programs. This is a complete solution: whenever a polynomial bound exists it will be found.

Programs that operate over recursive data structures may contain potential parallel computations. Writing parallel programs, even when aided by parallel skeletons, is very challenging, requires intricate analysis of the underlying algorithm and often uses inefficient intermediate data structures. Very few automated parallelisation methods that address a wide range of programs and data types exist. In this paper, we present a transformation method for functional programs defined over any recursive data types. Our method encodes the inputs of a program so that the transformed program is more likely to contain instances of polytypic fold skeletons, and less likely to contain inefficient intermediate data structures. With parallel implementations for these skeletons, the transformed programs can potentially be evaluated on hardware such as multi-core CPUs and/or GPUs.

This paper presents a model solution for controlling the execution of BPEL business processes based on reputation constraints at the level of the services, the service providers and the BPEL workflow. The reputation constraints are expressed as part of an SLA and are then enforced at runtime by a reputation monitoring system. We use our model to demonstrate how trust requirements based on such reputation constraints can be upheld in a real world example of a distributed map processing defined as a BPEL workflow.

In this paper, we provide an improved basis for the "distillation" program transformation. It is known that superlinear speedups can be obtained using distillation, but cannot be obtained by other earlier automatic program transformation techniques such as deforestation, positive supercompilation and partial evaluation. We give distillation an improved semantic basis, and explain how superlinear speedups can occur.

In this paper, we present a new transformation algorithm called distillation which can automatically transform higher-order functional programs into equivalent tail-recursive programs. Using this algorithm, it is possible to produce superlinear improvement in the runtime of programs. This represents a significant advance over the supercompilation algorithm, which can only produce a linear improvement. Outline proofs are given that the distillation algorithm is correct and that it always terminates.