cl-banner

Certifying Termination and Complexity Proofs of Programs


Termination (all computations produce a result) and complexity (how long does it take to get the result, and how much memory is required) are fundamental properties of programs. Although undecidable in general, much work has been spent on automated termination and complexity analysis. Whereas the answer to the question for a given program might be simple (yes, the program is terminating), the underlying proof is usually not that simple. In fact, most tools for automated complexity and termination analysis are complex tools, which combine several techniques while trying to analyze the behavior of a program. Consequently, these tools may contain errors and give wrong answers and proofs.

One solution to this problem is the usage of certifiers, which can check the proofs that are generated by the tools. For reliability, the soundness of the certifiers itself has to be formally proven within a theorem prover. Note that with the help of the certifiers, several bugs have been spotted, both in the implementations of the tools, as well as in soundness proofs of termination techniques. Unfortunately, so far the applicability of the available certifiers in this area is rather limited: they mainly handle termination proofs, but not complexity proofs; and they are limited to term rewriting, a simple computational model that underlies much of declarative programming and automated theorem proving.

In this project, we will extend the applicability of certifiers in two important directions: we want to support a large class of complexity proofs, and we want to support termination proofs for the widely used intermediate language LLVM via a translation to integer transition systems. To this end, we will develop several interesting formalizations. This includes a large library on linear algebra, which will be required for dealing with complexity proofs. Moreover, we will define a formal semantics of LLVM in Isabelle/HOL, and verify the translation from LLVM to integer transition systems. Finally, we will develop a certified SMT solver for linear integer arithmetic in order to validate termination proofs of integer transition systems.

Our work will drastically improve the reliability of current termination and complexity tools. Furthermore, it can serve as a starting point for performing other formalizations in the area of program analysis and program transformations.

Members


Current Members

  • Ralph Bottesch
  • Max W. Haslbeck
  • René Thiemann

Former Members

  • Sebastiaan Joosten
  • Christian Sternagel
  • Akihisa Yamada

 

FWF project number
Y757

  Contact
rene.thiemann@uibk.ac.at

Publications

Nach oben scrollen