KeYmaera X 中的化学案例研究

安全关键的化学过程是价值数十亿美元产业的支柱，因此社会理应获得最强有力的保证以确保其安全。为此，化学过程的模型在形式化方法文献中得到了广泛研究，包括结合离散与连续动力学的混合系统模型。本文首次使用 KeYmaera X 定理证明器，通过微分动态逻辑验证化学模型。我们的案例研究在以下结合方面具有新颖性：我们提供了强有力的一般情况正确性定理，使用了特别丰富的混合动力学，并具有特别严谨的证明。KeYmaera X 使这种新颖的结合成为可能。同时，我们讲述了关于 KeYmaera X 的一个普遍性故事：在微分方程安全性与活性的自动推理方面的最新进展，使得关于反应动力学的优雅证明成为可能。