Automated Theorem Proving with dL in Julia

Explore automated theorem proving for hybrid systems in this JuliaCon 2024 conference talk. Discover Elenchos, a Julia package designed to simplify the theorem proving process for hybrid system models. Learn how to translate ModelingToolkit.jl models into differential dynamic logic and interface with the KeYmaera X theorem prover for automatic verification of system properties. Delve into fundamental theorem proving concepts like loop invariants and quantifier elimination. Compare theorem proving with other verification methods such as simulation, reachability analysis, and manual analysis. Gain insights into the importance of formal verification for complex systems like cars, robots, and planes, where both continuous and discrete dynamics are present.

Automated Theorem Proving with dL in Julia | Hellwig | JuliaCon 2024