Search Results

Documents authored by Berry, Gérard

Document
DOI: 10.4230/LITES.10.1.2
Towards a Coq-verified Chain of Esterel Semantics

Authors: Lionel Rieg and Gérard Berry

Published in: LITES, Volume 10, Issue 1 (2025). Leibniz Transactions on Embedded Systems, Volume 10, Issue 1

Abstract
This article focuses on formally specifying and verifying the chain of formal semantics of the Esterel synchronous programming language using the Coq proof assistant. In particular, in addition to the standard logical (LBS) semantics, constructive semantics (CBS) and constructive state semantics (CSS), we introduce a novel microstep semantics that gets rid of the Must/Can potential function pair of the constructive semantics and can be viewed as an abstract version of Esterel’s circuit semantics used by compilers to generate software code and hardware designs. The article also comes with formal proofs in Coq of the equivalence between the CBS and CSS semantics and of the refinement of the CSS by the microstep semantics, except for the loop construct of Esterel.
Cite as

Lionel Rieg and Gérard Berry. Towards a Coq-verified Chain of Esterel Semantics. In LITES, Volume 10, Issue 1 (2025). Leibniz Transactions on Embedded Systems, Volume 10, Issue 1, pp. 2:1-2:54, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@Article{rieg_et_al:LITES.10.1.2,
  author =	{Rieg, Lionel and Berry, G\'{e}rard},
  title =	{{Towards a Coq-verified Chain of Esterel Semantics}},
  journal =	{Leibniz Transactions on Embedded Systems},
  pages =	{2:1--2:54},
  ISSN =	{2199-2002},
  year =	{2025},
  volume =	{10},
  number =	{1},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LITES.10.1.2},
  URN =		{urn:nbn:de:0030-drops-230144},
  doi =		{10.4230/LITES.10.1.2},
  annote =	{Keywords: Esterel programming language, formal verification, Coq proof assistant}
}
Document
DOI: 10.4230/DagSemRep.328
Synchronous Languages (Dagstuhl Seminar 01491)

Authors: Willem-Paul de Roever, Nicolas Halbwachs, Gérard Berry, and Klaus Winkelmann

Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)

Abstract
Cite as

Willem-Paul de Roever, Nicolas Halbwachs, Gérard Berry, and Klaus Winkelmann. Synchronous Languages (Dagstuhl Seminar 01491). Dagstuhl Seminar Report 328, pp. 1-30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2002)

Copy BibTex To Clipboard

@TechReport{deroever_et_al:DagSemRep.328,
  author =	{de Roever, Willem-Paul and Halbwachs, Nicolas and Berry, G\'{e}rard and Winkelmann, Klaus},
  title =	{{Synchronous Languages (Dagstuhl Seminar 01491)}},
  pages =	{1--30},
  ISSN =	{1619-0203},
  year =	{2002},
  type = 	{Dagstuhl Seminar Report},
  number =	{328},
  institution =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemRep.328},
  URN =		{urn:nbn:de:0030-drops-152119},
  doi =		{10.4230/DagSemRep.328},
}
Document
DOI: 10.4230/DagSemRep.104
Synchronous Languages (Dagstuhl Seminar 9448)

Authors: Gérard Berry, Willem-Paul de Roever, Axel Poigné, and Amir Pnueli

Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)

Abstract
Cite as

Gérard Berry, Willem-Paul de Roever, Axel Poigné, and Amir Pnueli. Synchronous Languages (Dagstuhl Seminar 9448). Dagstuhl Seminar Report 104, pp. 1-31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (1995)

Copy BibTex To Clipboard

@TechReport{berry_et_al:DagSemRep.104,
  author =	{Berry, G\'{e}rard and de Roever, Willem-Paul and Poign\'{e}, Axel and Pnueli, Amir},
  title =	{{Synchronous Languages (Dagstuhl Seminar 9448)}},
  pages =	{1--31},
  ISSN =	{1619-0203},
  year =	{1995},
  type = 	{Dagstuhl Seminar Report},
  number =	{104},
  institution =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemRep.104},
  URN =		{urn:nbn:de:0030-drops-149924},
  doi =		{10.4230/DagSemRep.104},
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact