Visualizing Counterexamples in Differential Dynamic Logic

When proving system properties in differential dynamic logic (dL), it’s often unclear whether a failed proof attempt is due to an actual system flaw or a missing proof step. Counterexamples can help, but understanding them in the abstract is challenging. This project explores integrating visualization tools to make counterexamples more intuitive, bridging the gap between formal reasoning and system behavior. If you’re interested in formal methods, visualization, and dynamical systems, this is a great opportunity to make proofs more insightful and interactive.

For more information, please reach out to jonathan.hellwig@kit.edu.