Servicenavigation

Project Details

Back

Projekt Print View

Automated Termination and Complexity Analysis of Imperative Programs

Subject Area Theoretical Computer Science
Term from 2013 to 2025
Project identifier Deutsche Forschungsgemeinschaft (DFG) - Project number 235950644
 
Final Report Year 2024

Final Report Abstract

Our goal was to analyze termination and complexity of imperative programs, which is crucial for software verification. We used the following methodology: In the front-end, a finite symbolic execution graph is generated from the program, which represents all possible program executions. Then, a program in a simple language, e.g., a term rewrite system (TRS) or an integer transition system (ITS) is synthesized from the graph. Finally, termination or complexity of this simple program is analyzed in the back-end of our approach. We obtained the following contributions: (A) Termination Analysis: Based on our previous work on termination of Java, we developed an approach for automatic termination analysis of C programs, which can analyze programs with low-level memory operations and features like dynamic data structures, recursion, or bitvector integers. While termination is undecidable in general, we also developed results on classes of programs where questions of termination or complexity are decidable. So for sub-programs from such a class, one can apply complete techniques. To improve the power of the back-end, we obtained several new results on termination of TRSs. We developed novel frameworks for relative termination and for almost-sure termination of probabilistic TRSs, and results on using termination analysis of TRSs to minimize description logic proofs. (B) Complexity Analysis (Upper Bounds): We adapted techniques for proving termination to infer upper bounds on the runtime of programs. This concerns both the front-ends for Java and C, and the back-ends for TRSs and ITSs. In particular, we developed a modular approach for complexity analysis of ITSs which alternates between computing runtime and size bounds (on the values of program variables) for program parts. To increase its power, we also integrated complete techniques (as in (A)) for sub-programs where runtime or size bounds are computable. Moreover, we adapted the approach in order to compute upper bounds on the expected runtimes of probabilistic ITSs. (C) Complexity Analysis (Lower Bounds): To detect bugs, we also developed techniques to compute lower runtime bounds for back-end programs. For ITSs, these techniques rely on accelerating loops into non-deterministic straight-line code. We developed new calculi to combine loop acceleration with the search for counterexamples in order to use loop acceleration not just for lower bounds, but also to prove non-termination of ITSs or (un)satisfiability of Constraint Horn Clauses (which are used to analyze program safety). Since loop acceleration often generates exponential expressions, to check reachability in accelerated programs, we also extended SMT solvers to exponential integer arithmetic. (D) Implementation: We implemented all our contributions in the tools AProVE (for the overall approach), KoAT and LoAT (for upper and lower bounds of ITSs), and SwInE (for SMT modulo exponential arithmetic). Their power was evaluated in extensive experiments and annual competitions.

Link to the final report

https://doi.org/10.34657/17569

Publications

 
 

Additional Information

© 2025 DFG Disclaimer / Copyright / Privacy Policy

Textvergrößerung und Kontrastanpassung