HDL defines dynamic theories with lifting and combination operations, proves soundness and relative completeness in Isabelle, and demonstrates the approach on a Java controller steering a differential dynamic logic plant model.
Differential Dynamic Logic for Hybrid Systems
2 Pith papers cite this work. Polarity classification is still indexing.
2
Pith papers citing it
citation-role summary
background 1
citation-polarity summary
fields
cs.LO 2roles
background 1polarities
background 1representative citing papers
Isabelle/HOL proofs establish conservation, monotonicity, compartment bounds, and threshold conditions for the SIR ODE by bridging AFP local flows to global forward solutions with reusable scalar lemmas.
citing papers explorer
-
Heterogeneous Dynamic Logic: Provability Modulo Program Theories
HDL defines dynamic theories with lifting and combination operations, proves soundness and relative completeness in Isabelle, and demonstrates the approach on a Java controller steering a differential dynamic logic plant model.
-
Certified Qualitative Analysis of the SIR ODE and Reusable Scalar Lemmas in Isabelle/HOL
Isabelle/HOL proofs establish conservation, monotonicity, compartment bounds, and threshold conditions for the SIR ODE by bridging AFP local flows to global forward solutions with reusable scalar lemmas.