2024-07-12 –, If (1.1)
In this talk, we introduce a Julia package that transforms hybrid system models into a formal language for theorem proving, providing a new tool to analyze your model. We explore how, with the help of our package, you can automatically find proofs to verify system properties. By explaining key concepts such as quantifier elimination and loop invariants, we show the core principles of proof search. Finally, we compare our approach to other methods in the Julia ecosystem.
In the realm of software engineering, uncovering bugs lurking within code can prove to be a challenging task. However, theorem proving offers a formal and rigorous approach to verifying program correctness, providing a valuable tool for software verification. This is particularly important in hybrid systems like cars, robots or planes, where both continuous and discrete dynamics are present.
As a system modeler, having theorem proving in your tool belt alongside other software verification techniques can be a useful addition to ensure the reliability and correctness of your code.
In this talk, we introduce Elenchos, a Julia package aimed at simplifying the theorem proving process for hybrid system models. Elenchos introduces a Julia macro that makes it easier to translate a model from ModelingToolkit.jl into differential dynamic logic, a formal language for verification of hybrid systems. Additionally, the package provides macros to interface with the theorem prover KeYmaera X to automatically verify system properties.
Throughout the talk, we explain the technologies behind proof automation by exploring fundamental theorem proving concepts such as loop invariants and quantifier elimination.
Furthermore, we will compare the theorem proving approach with other existing methods like simulation, reachability analysis, or manual analysis to highlight its unique advantages.
Join us as we explore the intricacies of theorem proving and its application in hybrid system verification.
I am a PhD student at KIT, Germany in the group logic of autonomous dynamical systems. I am interested in combining ideas of formal verification with numerical computation.