Galois connection based abstract interpretations for strictness analysis

Patrick Cousot, Radhia Cousot

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

Abstract

The abstract interpretation framework based upon the approximation of a fixpoint collecting semantics using Galois connections and widening/ narrowing operators on complete lattices [CC77a, CC79b] has been considered difficult to apply to Mycroft's strictness analysis [MycS0, MycS1] for which denotational semantics was though to be more adequate (because non-termination has to be taken into account), see e.g. [AH87], page 25. Considering a non-deterministic first-order language, we show, contrary to expectation, and using the classical Galois connection-based framework, that Mycroft strictness analysis algorithm is the abstract interpretation of a relational semantics (a big-steps operational semantics including non-termination which can be defined in G176 either in rule-based or fixpoint style by induction on the syntax of programs [CC92]) An improved version of Johnsson's algorithm [Joh81] is obtained by a subsequent dependence-free abstraction of Mycroft's dependence-sensitive method. Finally, a compromise between the precision of dependence-sensitive algorithms and the efficiency of dependence-free algorithms is suggested using widening operators.

Original languageEnglish (US)
Title of host publicationFormal Methods in Programming and Their Applications - International Conference, Proceedings
PublisherSpringer Verlag
Pages98-127
Number of pages30
Volume735 LNCS
ISBN (Print)9783540573166
StatePublished - 1993
Event1st International Conference on Formal Methods in Programming and their Applications, 1993 - Academgorodok, Novosibirsk, Russian Federation
Duration: Jun 28 1993Jul 2 1993

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume735 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other1st International Conference on Formal Methods in Programming and their Applications, 1993
CountryRussian Federation
CityAcademgorodok, Novosibirsk
Period6/28/937/2/93

Fingerprint

Galois Connection
Abstract Interpretation
Semantics
Fixpoint
Denotational Semantics
Algorithm Analysis
Complete Lattice
Operational Semantics
Operator
Mathematical operators
Proof by induction
First-order
Approximation
Framework

Keywords

  • Abstract interpretation
  • Dependence-free and dependence-sensitive analysis
  • Galois connection
  • Relational semantics
  • Strictness analysis
  • Widening

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Cousot, P., & Cousot, R. (1993). Galois connection based abstract interpretations for strictness analysis. In Formal Methods in Programming and Their Applications - International Conference, Proceedings (Vol. 735 LNCS, pp. 98-127). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 735 LNCS). Springer Verlag.

Galois connection based abstract interpretations for strictness analysis. / Cousot, Patrick; Cousot, Radhia.

Formal Methods in Programming and Their Applications - International Conference, Proceedings. Vol. 735 LNCS Springer Verlag, 1993. p. 98-127 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 735 LNCS).

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

Cousot, P & Cousot, R 1993, Galois connection based abstract interpretations for strictness analysis. in Formal Methods in Programming and Their Applications - International Conference, Proceedings. vol. 735 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 735 LNCS, Springer Verlag, pp. 98-127, 1st International Conference on Formal Methods in Programming and their Applications, 1993, Academgorodok, Novosibirsk, Russian Federation, 6/28/93.
Cousot P, Cousot R. Galois connection based abstract interpretations for strictness analysis. In Formal Methods in Programming and Their Applications - International Conference, Proceedings. Vol. 735 LNCS. Springer Verlag. 1993. p. 98-127. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
Cousot, Patrick ; Cousot, Radhia. / Galois connection based abstract interpretations for strictness analysis. Formal Methods in Programming and Their Applications - International Conference, Proceedings. Vol. 735 LNCS Springer Verlag, 1993. pp. 98-127 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{7936b6a1c6f140b3b52206c19848ba51,
title = "Galois connection based abstract interpretations for strictness analysis",
abstract = "The abstract interpretation framework based upon the approximation of a fixpoint collecting semantics using Galois connections and widening/ narrowing operators on complete lattices [CC77a, CC79b] has been considered difficult to apply to Mycroft's strictness analysis [MycS0, MycS1] for which denotational semantics was though to be more adequate (because non-termination has to be taken into account), see e.g. [AH87], page 25. Considering a non-deterministic first-order language, we show, contrary to expectation, and using the classical Galois connection-based framework, that Mycroft strictness analysis algorithm is the abstract interpretation of a relational semantics (a big-steps operational semantics including non-termination which can be defined in G∞176 either in rule-based or fixpoint style by induction on the syntax of programs [CC92]) An improved version of Johnsson's algorithm [Joh81] is obtained by a subsequent dependence-free abstraction of Mycroft's dependence-sensitive method. Finally, a compromise between the precision of dependence-sensitive algorithms and the efficiency of dependence-free algorithms is suggested using widening operators.",
keywords = "Abstract interpretation, Dependence-free and dependence-sensitive analysis, Galois connection, Relational semantics, Strictness analysis, Widening",
author = "Patrick Cousot and Radhia Cousot",
year = "1993",
language = "English (US)",
isbn = "9783540573166",
volume = "735 LNCS",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "98--127",
booktitle = "Formal Methods in Programming and Their Applications - International Conference, Proceedings",
address = "Germany",

}

TY - GEN

T1 - Galois connection based abstract interpretations for strictness analysis

AU - Cousot, Patrick

AU - Cousot, Radhia

PY - 1993

Y1 - 1993

N2 - The abstract interpretation framework based upon the approximation of a fixpoint collecting semantics using Galois connections and widening/ narrowing operators on complete lattices [CC77a, CC79b] has been considered difficult to apply to Mycroft's strictness analysis [MycS0, MycS1] for which denotational semantics was though to be more adequate (because non-termination has to be taken into account), see e.g. [AH87], page 25. Considering a non-deterministic first-order language, we show, contrary to expectation, and using the classical Galois connection-based framework, that Mycroft strictness analysis algorithm is the abstract interpretation of a relational semantics (a big-steps operational semantics including non-termination which can be defined in G∞176 either in rule-based or fixpoint style by induction on the syntax of programs [CC92]) An improved version of Johnsson's algorithm [Joh81] is obtained by a subsequent dependence-free abstraction of Mycroft's dependence-sensitive method. Finally, a compromise between the precision of dependence-sensitive algorithms and the efficiency of dependence-free algorithms is suggested using widening operators.

AB - The abstract interpretation framework based upon the approximation of a fixpoint collecting semantics using Galois connections and widening/ narrowing operators on complete lattices [CC77a, CC79b] has been considered difficult to apply to Mycroft's strictness analysis [MycS0, MycS1] for which denotational semantics was though to be more adequate (because non-termination has to be taken into account), see e.g. [AH87], page 25. Considering a non-deterministic first-order language, we show, contrary to expectation, and using the classical Galois connection-based framework, that Mycroft strictness analysis algorithm is the abstract interpretation of a relational semantics (a big-steps operational semantics including non-termination which can be defined in G∞176 either in rule-based or fixpoint style by induction on the syntax of programs [CC92]) An improved version of Johnsson's algorithm [Joh81] is obtained by a subsequent dependence-free abstraction of Mycroft's dependence-sensitive method. Finally, a compromise between the precision of dependence-sensitive algorithms and the efficiency of dependence-free algorithms is suggested using widening operators.

KW - Abstract interpretation

KW - Dependence-free and dependence-sensitive analysis

KW - Galois connection

KW - Relational semantics

KW - Strictness analysis

KW - Widening

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

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

M3 - Conference contribution

SN - 9783540573166

VL - 735 LNCS

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 98

EP - 127

BT - Formal Methods in Programming and Their Applications - International Conference, Proceedings

PB - Springer Verlag

ER -