Patrick Cousot and Radhia Cousot.<bR> An Abstract Interpretation Framework for Termination.

Patrick Cousot and Radhia Cousot.
An Abstract Interpretation Framework for Termination.
In Conference Record of the 39^th ACM SIGPLAN SIGACT Symposium on Principles of Programming Languages, Philadelphia, PA, USA, January 25—27, pp. 245—258 2012. © ACM Press, New York.
Letter paper format: PDF (1.5 Mb)
Abstract: 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.
     The abstract interpretation design principle is first illustrated for the design of new forward and backward proof, verification and analysis methods for safety. The safety collecting semantics defining the strongest safety property of programs is first expressed in a constructive fixpoint form. Safety proof and checking/verification methods then immediately follow by fixpoint induction. Static analysis of abstract safety properties such as invariance are constructively designed by fixpoint abstraction (or approximation) to (automatically) infer safety properties. So far, no such clear design principle did exist for termination so that the existing approaches are scattered and largely not comparable with each other.
     For (1), we show that this 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. F
     or (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.
Categories and Subject Descriptors: D.2.4 [Software/Program Verification];
D.3.1 [Formal Definitions and Theory];
F.3.1 [Specifying and Verifying and Reasoning about Programs].
General Terms: Languages, Reliability, Security, Theory, Verification.
Keywords: Abstract Interpretation, Induction, Proof, Safety, Static analysis, Variant function, Verification, Termination.
Slides of the 25mn POPL'12 presentation are available in US Letter 4 slides/page PDF (47.4 Mb)
A video of the 25mn POPL'12 presentation is available online

Bibliographic reference:

\bibitem{CousotCousot-POPL12}
P.~Cousot and R.~Cousot.
\newblock An Abstract Interpretation Framework for Termination.
\newblock In \emph{Conference Record of the 39$^{\mathrm{th}}$ Annual ACM
  SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
  pages 245--258, Philadelphia, PA, January 14-16, 2012. ACM Press, New York,
  NY.

@inproceedings{CousotCousot-POPL12,
   author =    {P.~Cousot and R.~Cousot},
   title =     {An Abstract Interpretation Framework for Termination},
   booktitle = {Conference Record of the 39$^{\mathrm{th}}$ Annual ACM 
                SIGPLAN-SIGACT Symposium on Principles of Programming 
                Languages},
   pages =     {245--258},
   address =   {Philadelphia, PA},
   publisher = {ACM Press, New York},
   month =     jan # " 25-27",
   year =      2012,
}

Copyright: © ACM, (2012). This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in Conference Record of the Thirtynineth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'12, January 25-27, 2012, Philadelphia, PA, USA. Copyright © 2012 ACM

copyright notice, ACM copyright
Last modified: Friday, 04-May-2012 10:01:26 EDT