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

Patrick Cousot

doi:10.1016/S1571-0661(05)80168-9

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

Patrick Cousot

Computer Science

Research output: Contribution to journal › Conference article › peer-review

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 language	English (US)
Pages (from-to)	77-102
Number of pages	26
Journal	Electronic Notes in Theoretical Computer Science
Volume	6
DOIs	https://doi.org/10.1016/S1571-0661(05)80168-9
State	Published - 1997
Event	MFPS XIII, Mathematical Foundations of Progamming Semantics, Thirteenth Annual Conference - Pittsburgh, PA, United States Duration: Mar 23 1997 → Mar 26 1997

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

10.1016/S1571-0661(05)80168-9

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",

note = "Copyright: Copyright 2008 Elsevier B.V., All rights reserved.; MFPS XIII, Mathematical Foundations of Progamming Semantics, Thirteenth Annual Conference ; Conference date: 23-03-1997 Through 26-03-1997",

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 - Conference article

AN - SCOPUS:18944390494

SN - 1571-0661

VL - 6

SP - 77

EP - 102

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

T2 - MFPS XIII, Mathematical Foundations of Progamming Semantics, Thirteenth Annual Conference

Y2 - 23 March 1997 through 26 March 1997

ER -

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

Abstract

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this