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

Other

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

Fingerprint

Static analysis
Semantics
Syntactics
Invariance

Keywords

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

ASJC Scopus subject areas

  • Software

Cite this

Cousot, P., & Cousot, R. (2012). An abstract interpretation framework for termination. In POPL'12 - Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (pp. 245-257) https://doi.org/10.1145/2103656.2103687

An abstract interpretation framework for termination. / Cousot, Patrick; Cousot, Radhia.

POPL'12 - Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 2012. p. 245-257.

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

Cousot, P & Cousot, R 2012, An abstract interpretation framework for termination. in POPL'12 - Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. pp. 245-257, 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'12, Philadelphia, PA, United States, 1/25/12. https://doi.org/10.1145/2103656.2103687
Cousot P, Cousot R. An abstract interpretation framework for termination. In POPL'12 - Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 2012. p. 245-257 https://doi.org/10.1145/2103656.2103687
Cousot, Patrick ; Cousot, Radhia. / An abstract interpretation framework for termination. POPL'12 - Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 2012. pp. 245-257
@inproceedings{10223f9f0bcf4714bb682de8ee3685bf,
title = "An abstract interpretation framework for termination",
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.",
keywords = "Abstract interpretation, Induction, Proof, Safety, Static analysis, Termination, Variant function, Verification",
author = "Patrick Cousot and Radhia Cousot",
year = "2012",
doi = "10.1145/2103656.2103687",
language = "English (US)",
isbn = "9781450310833",
pages = "245--257",
booktitle = "POPL'12 - Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages",

}

TY - GEN

T1 - An abstract interpretation framework for termination

AU - Cousot, Patrick

AU - Cousot, Radhia

PY - 2012

Y1 - 2012

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

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

KW - Abstract interpretation

KW - Induction

KW - Proof

KW - Safety

KW - Static analysis

KW - Termination

KW - Variant function

KW - Verification

UR - http://www.scopus.com/inward/record.url?scp=84857808844&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84857808844&partnerID=8YFLogxK

U2 - 10.1145/2103656.2103687

DO - 10.1145/2103656.2103687

M3 - Conference contribution

SN - 9781450310833

SP - 245

EP - 257

BT - POPL'12 - Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

ER -