一句话：在 Coq 中为带 reset 原语的数据流同步语言扩展机器化语义，并证明其编译器各趟的正确性。
基于块图与状态机的规约广泛用于安全关键控制软件，SCADE Suite 和 Simulink/Stateflow 等工具能将其编译为可执行代码，其核心语言如 Lustre 属于数据流同步语言。已有工作基于 CompCert 在 Coq 中为 Lustre 核心指定并验证编译器，将基于流的源语言语义与生成汇编的顺序内存操作形式化关联。本文扩展该工作以处理重置子系统这一原语。贡献包括：提出适合机器化推理的新语义规则，设计用于生成优化代码的新中间语言，并给出相关编译趟的正确性证明。该工作使带 reset 的同步数据流语言也能享有经过机器验证的编译正确性保证。
Specifications based on block diagrams and state machines are used to design control software, especially in the certified development of safety-critical applications. Tools like SCADE Suite and Simulink/Stateflow are equipped with compilers that translate such specifications into executable code. They provide programming languages for composing functions over streams as typified by Dataflow Synchronous Languages like Lustre. Recent work builds on CompCert to specify and verify a compiler for the core of Lustre in the Coq Interactive Theorem Prover. It formally links the stream-based semantics of the source language to the sequential memory manipulations of generated assembly code. We extend this work to treat a primitive for resetting subsystems. Our contributions include new semantic rules that are suitable for mechanized reasoning, a novel intermediate language for generating optimized code, and proofs of correctness for the associated compilation passes.
@article{paperbot551,
title = {Mechanized semantics and verified compilation for a dataflow synchronous language with reset},
author = {Timothy Bourke and Lélio Brun and Marc Pouzet},
journal = {Proceedings of the ACM on Programming Languages},
volume = {4},
number = {POPL},
year = {2019},
doi = {10.1145/3371112}
}