Deductive Verification for Ordinary Differential Equations
Abstract:
Cyber-physical systems (CPSs) feature software controllers interacting with real world physics. Correctness for such systems is paramount since they often operate in safety- or mission-critical settings. To verify correctness for a CPS, one first needs to have a model of its real world physics and methods for analyzing that model. In this talk, I will explain how ordinary differential equations (ODEs) models of CPS physics can be analyzed using a logical, deductive approach.
The first strength of this logical approach is enabling highly trustworthy, computer-checkable proofs of correctness properties for ODEs and CPSs. The second strength is its generality and flexibility, which I will exemplify through the deductive analysis of two key correctness properties for ODEs: safety and liveness. Safety of a system means it never reaches an undesirable (unsafe) state, while liveness means it eventually reaches a desirable (goal) state. This duality between safety and liveness is made precise through the lens of logic and it is their logical interplay which enables their analysis.
Biodata:
Yong Kiam Tan is a 5th year PhD student in Computer Science advised by Prof. Andre Platzer at Carnegie Mellon University. He is interested in the application of computer-assisted deductive verification in various domains. His thesis work investigates the design and usage of proof calculi for reasoning about ordinary differential equations. He is also an active developer of the verified CakeML compiler. He received his B.A. in Computer Science from Cambridge University.