Abstract
The research in this thesis is related to static cost and termination analysis.
Cost analysis aims at estimating the amount of resources that a given program
consumes during the execution, and termination analysis aims at proving that
the execution of a given program will eventually terminate. These analyses are
strongly related, indeed cost analysis techniques heavily rely on techniques developed for termination analysis. Precision, scalability, and applicability are essential in static analysis in general. Precision is related to the quality of the inferred
results, scalability to the size of programs that can be analyzed, and applicability
to the class of programs that can be handled by the analysis (independently from
precision and scalability issues). This thesis addresses these aspects in the context
of cost and termination analysis, from both practical and theoretical perspectives.
For cost analysis, we concentrate on the problem of solving cost relations (a
form of recurrence relations) into closed-form upper and lower bounds, which is
the heart of most modern cost analyzers, and also where most of the precision and
applicability limitations can be found. We develop tools, and their underlying
theoretical foundations, for solving cost relations that overcome the limitations of
existing approaches, and demonstrate superiority in both precision and applicability. A unique feature of our techniques is the ability to smoothly handle both
lower and upper bounds, by reversing the corresponding notions in the underlying theory. For termination analysis, we study the hardness of the problem of
deciding termination for a specific form of simple loops that arise in the context of
cost analysis. This study gives a better understanding of the (theoretical) limits
of scalability and applicability for both termination and cost analysis.
Keywords: Static analysis, Cost analysis, Termination analysis, Recurrence
equations, Complexity.