Automated Complexity Analysis via Transformations

This project is concerned with analysing the complexity of programs. This is a highly important subject, since the complexity of a program essentially determines its usefulness. We aim at an automated analysis that should work like a "push button" technology: we push a button and the tool gives us detailed information on the complexity of the input program. Furthermore we aim at a tool that performs a static program analysis and that can handle existing programming languages, not only toy languages. In recent years there have been several approaches to the automated analysis of the complexity of programs, for example in the field of embedded systems or in correctness proofs of program libraries. The first application is not surprisising: imagine a small program that is supposed to work efficiently on your smartphone: any unnecessary waste of resources has to be avoided and such a waste has to be detected before the program is distributed world- wide. In this project we will pursue the following aim: "Advance the state of the art of complexity analysis of programs by investigating automated runtime complexity analysis via transformations." Hence we will not pursue a direct approach, but rather a transformational one: First we will translate the input program into a term rewrite system and then we use the results obtained in the course of this project on the (automated) complexity analysis of rewrite systems. Thus we can exploit the simple and elegant framework provided by rewriting. Perhaps it is best to consider the analogy to SAT technology. In principle the question of satisfiability of a propositional formula is only of theoretical nature and may be considered a toy question. But after several breakthroughs in SAT solving and encodings theories SAT technology is now used as an arsenal for search techniques. Hardly any ad-hoc domain-specific algorithm outperforms a typical easy encoding into SAT and the use of an existing SAT solver. This is our vision, that eventually rewriting technology provides similar versatile and powerful tools for the complexity analysis of programs. We anticipate that the research described in this proposal will enhance the state of the art of complexity analysis of programs. It will significantly advance the state of the art in automated transformation techniques and automated complexity analysis in rewriting. Furthermore the project will impact research on amortised cost analysis, analysis of cost relations, and static program analysis in particular and implicit computational complexity and proof theory in general. In sum this project will bring us one step closer to a "push button" technology in the complexity analysis of realistic and large-scale programs.

The ACAT project is concerned with the verification of software. More precisely we have developed new and powerful methods in order to automatically verify whether an analysed software component or computer program can be executed within the provided resources. This is an incredible important area for information technology, as the use of resources of a program has repercussions on its usability. We are concerned in an automated analysis, which functions as a push-button technique. We press a button and the tool provides a detailed account on the resource usage of the analysed program. Furthermore, we are interested in static analysis, that is, an analysis which can already be employed within the development of the software. This method extends existing methods of profiling of programs. Finally, our concern are real programs written in existing programming languages. This aims at future applications of the methods developed in industry.Main results During the course of the project we developed methods, which allow us to analyse computer programs from a variety of application areas with respect to their required runtime and space bounds with a single uniform static analysis. This holds true for so- called imperative as well as declarative programs. Imperative programs follow an explicit command structure. Declarative programs are formulated more abstractly and can often be coded shorter. The mainstream of software is written in an imperative style. However, in recent years there is a strong trend towards the use of declarative languages. Our methods and in particular the developed analyser TCT are unique in their universal applicability. This universality shows itself clearly in international competitions. In these competitions TCT is always indicated as the most general and versatile prover. At the first FLoC Olympic Games, held within the Vienna Summer of Logic 2014, TCT could win a prestigious Kurt Gödel medal.Methodology Our approach to program analysis employs program transformations. First we abstract the given input program into a formally easily describable set of rules (a term rewrite system). This allows us to employ established methods for the resource analysis of term rewrite systems after the transformation. Due to this method we can exploit the technically simple and elegant approach of term rewrite systems. The universality of TCT is founded in this methodology.Factual informationThe ACAT project has been a stand-alone project for foundational research in the area of theoretical computer science and logic. Georg Moser has been the principal investigator.