Compositional and inductive semantic definitions in fixpoint, equational, constraint, closure-condition, rule-based and game-theoretic form

Patrick Cousot, Radhia Cousot

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

Abstract

We present a language and semantics-independent, compositional and inductive method for specifying formal semantics or semantic properties of programs in equivalent fixpoint, equational, constraint, closure-condition, rule-based and game-theoretic form. The definitional method is obtained by extending set-theoretic definitions in the context of partial orders. It is parameterized by the language syntax, by the semantic domains and by the semantic transformers corresponding to atomic and compound program components. The definitional method is shown to be preserved by abstract interpretation in either fixpoint, equational, constraint, closure-condition, rule-based or game-theoretic form. The features common to all possible instantiations are factored out thus allowing for results of general scope such as well-definedness, semantic equivalence, soundness and relative completeness of abstract interpretations, etc. to be proved compositionally in a general language and semantics-independent framework.

Original languageEnglish (US)
Title of host publicationComputer Aided Verification - 7th International Conference, CAV 1995, Proceedings
PublisherSpringer Verlag
Pages293-308
Number of pages16
Volume939
ISBN (Print)9783540600459
StatePublished - 1995
Event7th International Conference on Computer Aided Verification, CAV 1995 - Liege, Belgium
Duration: Jul 3 1995Jul 5 1995

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume939
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other7th International Conference on Computer Aided Verification, CAV 1995
CountryBelgium
CityLiege
Period7/3/957/5/95

Fingerprint

Fixpoint
Closure
Semantics
Game
Abstract Interpretation
Formal Semantics
Transformer
Soundness
Partial Order
Form
Completeness
Equivalence
Language

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Cite this

Cousot, P., & Cousot, R. (1995). Compositional and inductive semantic definitions in fixpoint, equational, constraint, closure-condition, rule-based and game-theoretic form. In Computer Aided Verification - 7th International Conference, CAV 1995, Proceedings (Vol. 939, pp. 293-308). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 939). Springer Verlag.

Compositional and inductive semantic definitions in fixpoint, equational, constraint, closure-condition, rule-based and game-theoretic form. / Cousot, Patrick; Cousot, Radhia.

Computer Aided Verification - 7th International Conference, CAV 1995, Proceedings. Vol. 939 Springer Verlag, 1995. p. 293-308 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 939).

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

Cousot, P & Cousot, R 1995, Compositional and inductive semantic definitions in fixpoint, equational, constraint, closure-condition, rule-based and game-theoretic form. in Computer Aided Verification - 7th International Conference, CAV 1995, Proceedings. vol. 939, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 939, Springer Verlag, pp. 293-308, 7th International Conference on Computer Aided Verification, CAV 1995, Liege, Belgium, 7/3/95.
Cousot P, Cousot R. Compositional and inductive semantic definitions in fixpoint, equational, constraint, closure-condition, rule-based and game-theoretic form. In Computer Aided Verification - 7th International Conference, CAV 1995, Proceedings. Vol. 939. Springer Verlag. 1995. p. 293-308. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
Cousot, Patrick ; Cousot, Radhia. / Compositional and inductive semantic definitions in fixpoint, equational, constraint, closure-condition, rule-based and game-theoretic form. Computer Aided Verification - 7th International Conference, CAV 1995, Proceedings. Vol. 939 Springer Verlag, 1995. pp. 293-308 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{cdc374896c984931bd80734f221950cc,
title = "Compositional and inductive semantic definitions in fixpoint, equational, constraint, closure-condition, rule-based and game-theoretic form",
abstract = "We present a language and semantics-independent, compositional and inductive method for specifying formal semantics or semantic properties of programs in equivalent fixpoint, equational, constraint, closure-condition, rule-based and game-theoretic form. The definitional method is obtained by extending set-theoretic definitions in the context of partial orders. It is parameterized by the language syntax, by the semantic domains and by the semantic transformers corresponding to atomic and compound program components. The definitional method is shown to be preserved by abstract interpretation in either fixpoint, equational, constraint, closure-condition, rule-based or game-theoretic form. The features common to all possible instantiations are factored out thus allowing for results of general scope such as well-definedness, semantic equivalence, soundness and relative completeness of abstract interpretations, etc. to be proved compositionally in a general language and semantics-independent framework.",
author = "Patrick Cousot and Radhia Cousot",
year = "1995",
language = "English (US)",
isbn = "9783540600459",
volume = "939",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "293--308",
booktitle = "Computer Aided Verification - 7th International Conference, CAV 1995, Proceedings",

}

TY - GEN

T1 - Compositional and inductive semantic definitions in fixpoint, equational, constraint, closure-condition, rule-based and game-theoretic form

AU - Cousot, Patrick

AU - Cousot, Radhia

PY - 1995

Y1 - 1995

N2 - We present a language and semantics-independent, compositional and inductive method for specifying formal semantics or semantic properties of programs in equivalent fixpoint, equational, constraint, closure-condition, rule-based and game-theoretic form. The definitional method is obtained by extending set-theoretic definitions in the context of partial orders. It is parameterized by the language syntax, by the semantic domains and by the semantic transformers corresponding to atomic and compound program components. The definitional method is shown to be preserved by abstract interpretation in either fixpoint, equational, constraint, closure-condition, rule-based or game-theoretic form. The features common to all possible instantiations are factored out thus allowing for results of general scope such as well-definedness, semantic equivalence, soundness and relative completeness of abstract interpretations, etc. to be proved compositionally in a general language and semantics-independent framework.

AB - We present a language and semantics-independent, compositional and inductive method for specifying formal semantics or semantic properties of programs in equivalent fixpoint, equational, constraint, closure-condition, rule-based and game-theoretic form. The definitional method is obtained by extending set-theoretic definitions in the context of partial orders. It is parameterized by the language syntax, by the semantic domains and by the semantic transformers corresponding to atomic and compound program components. The definitional method is shown to be preserved by abstract interpretation in either fixpoint, equational, constraint, closure-condition, rule-based or game-theoretic form. The features common to all possible instantiations are factored out thus allowing for results of general scope such as well-definedness, semantic equivalence, soundness and relative completeness of abstract interpretations, etc. to be proved compositionally in a general language and semantics-independent framework.

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

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

M3 - Conference contribution

SN - 9783540600459

VL - 939

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 293

EP - 308

BT - Computer Aided Verification - 7th International Conference, CAV 1995, Proceedings

PB - Springer Verlag

ER -