Chemical Case Studies in KeYmaera X

TL;DR

This paper demonstrates the application of KeYmaera X theorem-prover to verify safety properties of complex chemical process models using differential dynamic logic, showcasing its capabilities for rigorous hybrid systems verification.

Contribution

It is the first to verify chemical models with KeYmaera X, combining strong correctness theorems, rich hybrid dynamics, and rigorous proofs in this domain.

Findings

Successful verification of chemical process models.

KeYmaera X enabled elegant proofs of reaction dynamics.

Highlights advances in automated reasoning for differential equations.

Abstract

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.