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
EditorsDines Bjorner, Manfred Broy, Igor V. Pottosin
PublisherSpringer Verlag
Pages98-127
Number of pages30
ISBN (Print)9783540573166
DOIs
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

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)

Fingerprint Dive into the research topics of 'Galois connection based abstract interpretations for strictness analysis'. Together they form a unique fingerprint.

  • 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