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.
An Introduction to CORA 2015
2 Pith papers cite this work. Polarity classification is still indexing.
2
Pith papers citing it
citation-role summary
background 2
citation-polarity summary
years
2026 2roles
background 2polarities
background 2representative citing papers
Optimizing blended-wing-body aircraft wing half-spans via reachable sets of linear longitudinal dynamics yields up to 30% lower angle-of-attack tracking error on the resulting nonlinear model under reference tracking control.
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.
-
Reachability-Based Design Optimization for Aircraft Maneuverability
Optimizing blended-wing-body aircraft wing half-spans via reachable sets of linear longitudinal dynamics yields up to 30% lower angle-of-attack tracking error on the resulting nonlinear model under reference tracking control.