迈向经 Coq 验证的 Esterel 语义链
形式语言与自动机理论
2025-01-08 v4 计算机科学中的逻辑
编程语言
摘要
本文关注使用 Coq 证明助手对 Esterel 同步编程语言的正式语义链进行形式化规约与验证。特别地，除标准的逻辑（LBS）语义、构造语义（CBS）和构造状态语义（CSS）外，我们引入了一种新颖的微步语义，其去除了构造语义中的 Must/Can 势函数对，并可视为 Esterel 电路语义的抽象版本，后者被编译器用于生成软件代码与硬件设计。在排除 Esterel 的 loop 构造后，本文还在 Coq 中给出了 CBS 与 CSS 语义等价性以及 CSS 被微步语义精化形式化证明。
引用
@article{arxiv.1909.12582,
title = {Towards a Coq-verified Chain of Esterel Semantics},
author = {Gérard Berry and Lionel Rieg},
journal= {arXiv preprint arXiv:1909.12582},
year = {2025}
}