One of the main features of programs is the amount of resources which are needed in order to run them. Different resources can be taken into consideration, such as the number of execution steps, amount of memory allocated, number of calls to certain methods, etc. Unfortunately, manually determining the resource consumption of programs is difficult and error-prone. We provide an overview of a state of the art framework for automatically obtaining both upper and lower bounds on the resource consumption of programs. The bounds obtained are functions on the size of the input arguments to the program and are obtained statically, i.e., without running the program. Due to the approximations introduced, the framework can fail to obtain (non-trivial) bounds even if they exist. On the other hand, modulo implementation bugs, the bounds thus obtained are valid for any execution of the program. The framework has been implemented in the COSTA system and can provide useful bounds for realistic object-oriented and actor-based concurrent programs.
Abstract TBA.
Rewrite systems form an attractive model of computation. In the past decades numerous methods have been developed to prove rewrite systems terminating. Spurred by the International Termination Competition, the emphasis in recent years is on powerful methods that can be automated. Termination is a prerequisite, but to ensure that normal forms can be effectively computed, one needs termination methods from which a polynomial upper bound on the lengths of computations can be inferred. Until recently, very few results of this kind were known: If termination of a rewrite system can be established by a strongly linear interpretation or by the match-bound technique, there is a linear upper bound on the derivational complexity. The recent matrix method radically changed the picture. Using results from linear algebra (joint spectral radius theory) and weighted automata (degrees of ambiguity), conditions on matrix interpretation can be formulated to ensure a polynomial upper bound on the derivational complexity. These conditions can be translated into finite-domain constraint systems and solved by state-of-the-art SAT/SMT solvers.
Abstract TBA.