An abstract interpretation framework for termination

Patrick Cousot, Radhia Cousot

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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. 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.

Original languageEnglish (US)
Title of host publicationPOPL'12 - Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
Pages245-257
Number of pages13
DOIs
StatePublished - 2012
Event39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'12 - Philadelphia, PA, United States
Duration: Jan 25 2012Jan 27 2012

Publication series

NameConference Record of the Annual ACM Symposium on Principles of Programming Languages
ISSN (Print)0730-8566

Other

Other39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'12
CountryUnited States
CityPhiladelphia, PA
Period1/25/121/27/12

Keywords

  • Abstract interpretation
  • Induction
  • Proof
  • Safety
  • Static analysis
  • Termination
  • Variant function
  • Verification

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'An abstract interpretation framework for termination'. Together they form a unique fingerprint.

Cite this