<html><head><!-- CousotCousot-Venezia-2012-03-12.shtml --> <title>P. Cousot. Termination Proof Inference by Abstract Interpretation (joint work with R. Cousot)</title> <meta name="Keyword" content="Abstract Interpretation, Static analysis, Termination Proof, Variant Function"> </head> <body> <hr> <ul> <li> <strong>Patrick Cousot (joint work with Radhia Cousot).<br> <a href="COUSOTtalks/CousotCousot-Venezia-2012-03-12.shtml">Termination Proof Inference by Abstract Interpretation</A>.<br> </strong> Invited Talk, Computer Science PhD Day, Aula Magna Silvio Trentin, Universit&aacute; Ca' Foscari di Venezia, Italy, March 12<SUP>th</SUP>, 2012. <p> </p> </li> <li><em>Abstract:</em> <br>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;The existing approaches to termination proof are scattered and largely not comparable with each other. <br>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;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. <br>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;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. <br>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;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. <br>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;Joint work with Radhia Cousot. <P></P> </li> <li><em>Slides of the 55&nbsp;mn presentation</em> (to be used with <a href="http://get.adobe.com/reader/">Acrobat Reader</a>): <a href="../publications.www/slides-public/SlidesVeneziaCousotCousotTermination-4-1.pdf">.pdf</a>.</li> <p> </p> </li> <li><em>Bibliographic reference:</em> <pre> \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}, } </pre> <p> </p></li> <li><em>Pictures of the Aula Magna Silvio Trentin and Universit&aacute; Ca' Foscari:</em> <TABLE> <TR> <TD><IMG SRC="2012-03-12-Venezia-Photos/Venezia-L1013810.jpg" ORDER="0" ALIGN="MIDDLE" HSPACE="0" VSPACE="5"></TD> <TD><IMG SRC="2012-03-12-Venezia-Photos/Venezia-L1013809.jpg" ORDER="0" ALIGN="MIDDLE" HSPACE="0" VSPACE="5"></TD> </TR> <TR> <TD><IMG SRC="2012-03-12-Venezia-Photos/Venezia-L1013806.jpg" ORDER="0" ALIGN="MIDDLE" HSPACE="0" VSPACE="5"></TD> <TD><IMG SRC="2012-03-12-Venezia-Photos/Venezia-L1013803.jpg" ORDER="0" ALIGN="MIDDLE" HSPACE="0" VSPACE="5"></TD> </TR> <TR> <TD><IMG SRC="2012-03-12-Venezia-Photos/Venezia-L1007469.jpg" ORDER="0" ALIGN="MIDDLE" HSPACE="0" VSPACE="5"></TD> <TD><IMG SRC="2012-03-12-Venezia-Photos/Venezia-L1006897.jpg" ORDER="0" ALIGN="MIDDLE" HSPACE="0" VSPACE="5"></TD> </TR> </TABLE> </ul> </body> <hr> <b><a href=copyright.shtml#copyrightnotice">Copyright notice</a></b><BR> <br><b>Last modified:</b> <!--#echo var="LAST_MODIFIED" --> <hr> </html>