Towards a Coq-verified Chain of Esterel Semantics
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 (CS...
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
2025-04-01
|
| Series: | Leibniz Transactions on Embedded Systems |
| Subjects: | |
| Online Access: | https://drops.dagstuhl.de/storage/07lites/lites_vol010/lites_vol010_issue001/LITES.10.1.2/LITES.10.1.2.pdf |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1849706458709491712 |
|---|---|
| author | Rieg, Lionel Berry, Gérard |
| author_facet | Rieg, Lionel Berry, Gérard |
| author_sort | Rieg, Lionel |
| collection | DOAJ |
| description | 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. |
| format | Article |
| id | doaj-art-a50fdf345433447a87340f1dda000b2e |
| institution | DOAJ |
| issn | 2199-2002 |
| language | English |
| publishDate | 2025-04-01 |
| publisher | Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik |
| record_format | Article |
| series | Leibniz Transactions on Embedded Systems |
| spelling | doaj-art-a50fdf345433447a87340f1dda000b2e2025-08-20T03:16:11ZengSchloss Dagstuhl -- Leibniz-Zentrum fuer InformatikLeibniz Transactions on Embedded Systems2199-20022025-04-011012:12:5410.4230/LITES.10.1.2Towards a Coq-verified Chain of Esterel SemanticsRieg, Lionel0https://orcid.org/0009-0001-5751-3806Berry, Gérard1Université Grenoble Alpes, CNRS, Grenoble INP - UGA, VERIMAG, Grenoble, FranceCollège de France, Paris, FranceThis 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.https://drops.dagstuhl.de/storage/07lites/lites_vol010/lites_vol010_issue001/LITES.10.1.2/LITES.10.1.2.pdfesterel programming languageformal verificationcoq proof assistant |
| spellingShingle | Rieg, Lionel Berry, Gérard Towards a Coq-verified Chain of Esterel Semantics Leibniz Transactions on Embedded Systems esterel programming language formal verification coq proof assistant |
| title | Towards a Coq-verified Chain of Esterel Semantics |
| title_full | Towards a Coq-verified Chain of Esterel Semantics |
| title_fullStr | Towards a Coq-verified Chain of Esterel Semantics |
| title_full_unstemmed | Towards a Coq-verified Chain of Esterel Semantics |
| title_short | Towards a Coq-verified Chain of Esterel Semantics |
| title_sort | towards a coq verified chain of esterel semantics |
| topic | esterel programming language formal verification coq proof assistant |
| url | https://drops.dagstuhl.de/storage/07lites/lites_vol010/lites_vol010_issue001/LITES.10.1.2/LITES.10.1.2.pdf |
| work_keys_str_mv | AT rieglionel towardsacoqverifiedchainofesterelsemantics AT berrygerard towardsacoqverifiedchainofesterelsemantics |