Galois connection based abstract interpretations for strictness analysis

Patrick Cousot; Radhia Cousot

doi:10.1007/bfb0039703

Galois connection based abstract interpretations for strictness analysis

Patrick Cousot, Radhia Cousot

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference 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 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.

Original language	English (US)
Title of host publication	Formal Methods in Programming and Their Applications - International Conference, Proceedings
Editors	Dines Bjorner, Manfred Broy, Igor V. Pottosin
Publisher	Springer Verlag
Pages	98-127
Number of pages	30
ISBN (Print)	9783540573166
DOIs	https://doi.org/10.1007/bfb0039703
State	Published - 1993
Event	1st International Conference on Formal Methods in Programming and their Applications, 1993 - Academgorodok, Novosibirsk, Russian Federation Duration: Jun 28 1993 → Jul 2 1993

Publication series

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

Other

Other	1st International Conference on Formal Methods in Programming and their Applications, 1993
Country/Territory	Russian Federation
City	Academgorodok, Novosibirsk
Period	6/28/93 → 7/2/93

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)

Access to Document

10.1007/bfb0039703

Cite this

Cousot, P., & Cousot, R. (1993). Galois connection based abstract interpretations for strictness analysis. In D. Bjorner, M. Broy, & I. V. Pottosin (Eds.), Formal Methods in Programming and Their Applications - International Conference, Proceedings (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. https://doi.org/10.1007/bfb0039703

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

Formal Methods in Programming and Their Applications - International Conference, Proceedings. ed. / Dines Bjorner; Manfred Broy; Igor V. Pottosin. 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 proceeding › Conference contribution

Cousot, P & Cousot, R 1993, Galois connection based abstract interpretations for strictness analysis. in D Bjorner, M Broy & IV Pottosin (eds), Formal Methods in Programming and Their Applications - International Conference, Proceedings. 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. https://doi.org/10.1007/bfb0039703

Cousot P, Cousot R. Galois connection based abstract interpretations for strictness analysis. In Bjorner D, Broy M, Pottosin IV, editors, Formal Methods in Programming and Their Applications - International Conference, Proceedings. Springer Verlag. 1993. p. 98-127. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/bfb0039703

Cousot, Patrick ; Cousot, Radhia. / Galois connection based abstract interpretations for strictness analysis. Formal Methods in Programming and Their Applications - International Conference, Proceedings. editor / Dines Bjorner ; Manfred Broy ; Igor V. Pottosin. 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",

note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 1993.; 1st International Conference on Formal Methods in Programming and their Applications, 1993 ; Conference date: 28-06-1993 Through 02-07-1993",

year = "1993",

doi = "10.1007/bfb0039703",

language = "English (US)",

isbn = "9783540573166",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "98--127",

editor = "Dines Bjorner and Manfred Broy and Pottosin, {Igor V.}",

booktitle = "Formal Methods in Programming and Their Applications - International Conference, Proceedings",

}

TY - GEN

T1 - Galois connection based abstract interpretations for strictness analysis

AU - Cousot, Patrick

AU - Cousot, Radhia

N1 - Publisher Copyright: © Springer-Verlag Berlin Heidelberg 1993.

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

U2 - 10.1007/bfb0039703

DO - 10.1007/bfb0039703

M3 - Conference contribution

AN - SCOPUS:33749230178

SN - 9783540573166

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

A2 - Bjorner, Dines

A2 - Broy, Manfred

A2 - Pottosin, Igor V.

PB - Springer Verlag

T2 - 1st International Conference on Formal Methods in Programming and their Applications, 1993

Y2 - 28 June 1993 through 2 July 1993

ER -

Galois connection based abstract interpretations for strictness analysis

Abstract

Publication series

Other

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this