Jonathan Hellwig
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.
Session
07-12
16:30
30min
Automated Theorem Proving with dL in Julia
Jonathan Hellwig
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.
Math(s)
If (1.1)