AI 中文总结
研究为同步程序生成滴答索引证明义务的问题，核心方法是用标准自动机理论归约将LTL公式转换为坏状态自动机与程序形成积并导出义务，主要贡献是形式化原理、证明正确性及通过医疗输液控制器展示工作流程。
AI 中文摘要
同步程序的需求涉及跨滴答的观察，而通用演绎后端使用关于局部步骤的一阶条件。Kairos是一个原型工具链，可从同步程序和假设-保证形式的源级时态安全契约生成此类义务。它使用标准自动机理论归约，将线性时态逻辑（LTL）公式转换为坏状态自动机，与程序形成其积，并导出滴答索引的Why3义务。我们形式化了基本原理并证明了反应式契约的正确性。在Rocq中对定义、义务构造和证明进行了机械化。一个医疗输液控制器说明了工作流程。
英文摘要
Requirements for synchronous programs relate observations across ticks, while general-purpose deductive backends use first-order conditions on local steps. Kairos is a prototype toolchain generating such obligations from synchronous programs and source-level temporal safety contracts in assume-guarantee form. Using the standard automata-theoretic reduction, it translates their linear temporal logic (LTL) formulas into bad-state automata, forms their product with the program, and derives tick-indexed Why3 obligations. We formalize the underlying principles and prove reactive contract correctness: under the stated program and automaton hypotheses, every input trace satisfying the environment assumptions induces a unique execution satisfying the temporal guarantees. The definitions, obligation construction, and proof are mechanized in Rocq. A medical infusion controller illustrates the workflow.
Comments18 pages, 1 listing, 1 table. Submitted to VSTTE 2026
