Vehicle enables compositional verification of neural controllers in discrete and continuous cyber-physical systems across Rocq, Isabelle/HOL, Agda, and Imandra, including the first infinite time-horizon safety proof for a continuous medical device in a general-purpose ITP.
KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems
3 Pith papers cite this work. Polarity classification is still indexing.
3
Pith papers citing it
citation-role summary
background 3
citation-polarity summary
years
2026 3roles
background 3polarities
background 3representative citing papers
dARL supplies a sound deductive refinement calculus with trace semantics for verifying and simplifying differential-algebraic programs, shown complete for index reduction certification.
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
-
Compositional Neural-Cyber-Physical System Verification in the Interactive Theorem Prover of Your Choice
Vehicle enables compositional verification of neural controllers in discrete and continuous cyber-physical systems across Rocq, Isabelle/HOL, Agda, and Imandra, including the first infinite time-horizon safety proof for a continuous medical device in a general-purpose ITP.
-
A Deductive Refinement Calculus for Differential-Algebraic Programs
dARL supplies a sound deductive refinement calculus with trace semantics for verifying and simplifying differential-algebraic programs, shown complete for index reduction certification.
-
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.