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!
|