Galois connection based abstract interpretations for strictness analysis

Patrick Cousot, Radhia Cousot

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


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
Number of pages30
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


Other1st International Conference on Formal Methods in Programming and their Applications, 1993
Country/TerritoryRussian Federation
CityAcademgorodok, Novosibirsk


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

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


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

Cite this