Automated Termination and Complexity Analysis of Imperative Programs

• Applicant: Professor Dr. Jürgen Giesl
• Subject Area: Theoretical Computer Science
• Term: from 2013 to 2024
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 235950644

Our goal is to analyze the termination and complexity of programs in imperative languages like Java and C automatically. Such analyses are crucial for software construction and verification. In the first Phase of the project we developed the following methodology: First, in the front-end of our approach, a symbolic execution graph is automatically generated from the program. This graph is a finite representation of all possible executions of the Java or C program.Afterwards, a program in a simple language (e.g., an integer Transition system or a term rewrite system) is automatically generated from the graph. Finally, the termination or complexity of this generated simple program is analyzed (in the back-end of our approach). The results of the first project phase show the success of this methodology. In the proposed second phase, the approach will be developed further in order to make it applicable in practice. To this end, the project will tackle the following tasks: (A) There are important classes ofprograms where the previously developed techniques for Termination analysis cannot be used. Thus, these techniques have to be Extended accordingly and their modularity needs to be improved in order to make them applicable to large programs. (B) We showed that thetechniques for proving termination can be adapted such that they can infer upper complexity bounds for the runtime of programs. However, the adaptions developed in the first project phase often result in unnecessarily high bounds. Thus, the precision and the applicability of the approach need to be improved significantly. (C) In the first Phase of the project, we also developed techniques to compute lower complexity bounds for the runtime of the back-end programs. Now the goal is to develop these techniques further in order to use them forlanguages like Java and C in the front-end as well. (D) All contributions developed in (A) – (C) will be implemented in our verification tools AProVE, KoAT, and LoAT. Their power andperformance will be evaluated empirically and compared to other Tools in extensive experiments.

• DFG Programme: Research Grants