论文标题
Keymaera X中的化学案例研究
Chemical Case Studies in KeYmaera X
论文作者
论文摘要
安全 - 关键的化学过程是数十亿美元行业的骨干，因此社会应得到最强大的确保安全性。为此，化学过程的模型在形式方法文献中进行了充分研究，包括结合离散和连续动态的混合系统模型。本文是第一个使用keymaera x定理 - 示威者来验证具有差异动态逻辑的化学模型的文章。我们的案例研究在结合以下方面是新颖的：我们提供了强大的通用案例正确性定理，使用特别丰富的混合动力学，并具有特别严格的证明。 Keymaera X使这种新颖的组合成为可能。 同时，我们讲述了一个关于Keymaera X的一般故事：关于微分方程的安全性和易感性的自动推理的最新进展已实现了有关反应动态的优雅证明。
Safety-critical chemical processes are the backbone of multi-billion-dollar industries, thus society deserves the strongest possible guarantees that they are safe. To that end, models of chemical processes are well-studied in the formal methods literature, including hybrid systems models which combine discrete and continuous dynamics. This paper is the first to use the KeYmaera X theorem-prover to verify chemical models with differential dynamic logic. Our case studies are novel in combining the following: we provide strong general-case correctness theorems, use particularly rich hybrid dynamics, and have particularly rigorous proofs. This novel combination is made possible by KeYmaera X. Simultaneously, we tell a general story about KeYmaera X: recent advances in automated reasoning about safety and liveness for differential equations have enabled elegant proofs about reaction dynamics.
