Constructive design of a hierarchy of semantics of a transition system by abstract interpretation (Extended abstract)

Research output: Contribution to journalArticle

Abstract

We construct a hierarchy of semantics by successive abstract interpretations. Starting from a maximal trace semantics of a transition system, we derive a big-step semantics, termination and nontermination semantics, natural, demoniac and angelic relational semantics and equivalent nondeterministic denotational semantics, D. Scott's deterministic denotational semantics, generalized/conservative/liberal predicate transformer semantics, generalized/total/partial correctness axiomatic semantics and corresponding proof methods. All semantics are presented in uniform fixpoint form and the correspondence between these semantics are established through composable Galois connection.

Original languageEnglish (US)
Pages (from-to)77-102
Number of pages26
JournalElectronic Notes in Theoretical Computer Science
Volume6
DOIs
StatePublished - 1997

Fingerprint

Abstract Interpretation
Transition Systems
Semantics
Denotational Semantics
Galois Connection
Hierarchy
Design
Fixpoint
Transformer
Predicate
Termination
Correctness
Correspondence
Trace
Partial

ASJC Scopus subject areas

  • Computer Science (miscellaneous)

Cite this

@article{6a00c4e9d80a4ca6a24e10647a2c4068,
title = "Constructive design of a hierarchy of semantics of a transition system by abstract interpretation (Extended abstract)",
abstract = "We construct a hierarchy of semantics by successive abstract interpretations. Starting from a maximal trace semantics of a transition system, we derive a big-step semantics, termination and nontermination semantics, natural, demoniac and angelic relational semantics and equivalent nondeterministic denotational semantics, D. Scott's deterministic denotational semantics, generalized/conservative/liberal predicate transformer semantics, generalized/total/partial correctness axiomatic semantics and corresponding proof methods. All semantics are presented in uniform fixpoint form and the correspondence between these semantics are established through composable Galois connection.",
author = "Patrick Cousot",
year = "1997",
doi = "10.1016/S1571-0661(05)80168-9",
language = "English (US)",
volume = "6",
pages = "77--102",
journal = "Electronic Notes in Theoretical Computer Science",
issn = "1571-0661",
publisher = "Elsevier",

}

TY - JOUR

T1 - Constructive design of a hierarchy of semantics of a transition system by abstract interpretation (Extended abstract)

AU - Cousot, Patrick

PY - 1997

Y1 - 1997

N2 - We construct a hierarchy of semantics by successive abstract interpretations. Starting from a maximal trace semantics of a transition system, we derive a big-step semantics, termination and nontermination semantics, natural, demoniac and angelic relational semantics and equivalent nondeterministic denotational semantics, D. Scott's deterministic denotational semantics, generalized/conservative/liberal predicate transformer semantics, generalized/total/partial correctness axiomatic semantics and corresponding proof methods. All semantics are presented in uniform fixpoint form and the correspondence between these semantics are established through composable Galois connection.

AB - We construct a hierarchy of semantics by successive abstract interpretations. Starting from a maximal trace semantics of a transition system, we derive a big-step semantics, termination and nontermination semantics, natural, demoniac and angelic relational semantics and equivalent nondeterministic denotational semantics, D. Scott's deterministic denotational semantics, generalized/conservative/liberal predicate transformer semantics, generalized/total/partial correctness axiomatic semantics and corresponding proof methods. All semantics are presented in uniform fixpoint form and the correspondence between these semantics are established through composable Galois connection.

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

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

U2 - 10.1016/S1571-0661(05)80168-9

DO - 10.1016/S1571-0661(05)80168-9

M3 - Article

AN - SCOPUS:18944390494

VL - 6

SP - 77

EP - 102

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

SN - 1571-0661

ER -