Abstract:

This thesis is about automatic analysis of the complexity of programs, especially the complexity of the function computed rather than the complexity of the algorithm implemented.

First, termination orderings are restricted by the mean of quasi-interpretations, allowing one to give a bound on the complexity of the computed function. The system itself may compute in a time significantly larger than this bound, so it may be necessary to automatically transform the system in order to achieve the bound. In this way, a characterisation of both Ptime and Pspace are obtained.

Then, a small assembly-like language is studied via Petri nets. This allows a single analysis to do at the same time a termination proof close to the Size-Change Principle, a proof of the Non-Size Increasingness of the program and a simplification similar to Deforestation. Moreover, this technique is able to prove the termination of a wide class of programs. Especially, the termination of algorithms such as Euclid's one or the ``Divide and Conquer'' algorithms is obtained in a fully automated way.