Termination Proof Inference by Abstract Interpretation.
Invited Talk, Computer Science PhD Day, Aula Magna Silvio Trentin, Universitá Ca' Foscari di Venezia, Italy, March 12th, 2012.
The existing approaches to termination proof are scattered and largely not comparable with each other.
We introduce a unifying design principle for termination based on an abstract interpretation of a complete infinitary trace semantics. We show that proof, verification and analysis methods for termination all rely on two induction principles: (1) a variant function or induction on data ensuring progress towards the end and (2) some form of induction on the program structure.
For (1), we show that the abstract interrpetation-based design principle applies equally well to potential and definite termination. The trace-based termination collecting semantics is given a fixpoint definition. Its abstraction yields a fixpoint definition of the best variant function. By further abstraction of this best variant function, we derive the Floyd/Turing termination proof method as well as new static analysis methods to effectively compute approximations of this best variant function.
For (2), we introduce a generalization of the syntactic notion of structural induction (as found in Hoare logic) into a ``semantic structural induction'' based on the new semantic concept of inductive trace cover covering execution traces by ``segments'', a new basis for formulating program properties. Its abstractions allow for generalized recursive proof, verification and static analysis methods by induction on both program structure, control, and data. Examples of particular instances include Floyd's handling of loop cut-points as well as nested loops, Burstall's intermittent assertion total correctness proof method, and Podelski-Rybalchenko transition invariants.
Joint work with Radhia Cousot.
\bibitem{CousotCousotTermination-Venezia-2012-03-12}
P. Cousot.
\newblock Termination Proof Inference by Abstract Interpretation (joint work with R. Cousot).
\newblock \emph{Invited talk}, Computer Science PhD Day, Aula Magna Silvio Trentin,
Universit\`a Ca' Foscari di Venezia, Italy. 12 March 2012.
@inProceedings{CousotCousotTermination-Venezia-2012-03-12,
author = {P{.} Cousot},
title = {Termination Proof Inference by Abstract Interpretation (joint work with R. Cousot)},
booktitle = {Computer Science PhD Day, Aula Magna Silvio Trentin,
Universit\`a Ca' Foscari},
address = {Venezia, Italy},
month = {12 March},
year = {2012},
}
 |
 |
 |
 |
 |
 |