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.
Paulson, and Markus Wenzel
5 Pith papers cite this work. Polarity classification is still indexing.
5
Pith papers citing it
citation-role summary
background 4
citation-polarity summary
years
2026 5roles
background 4polarities
background 4representative citing papers
Hyper Separation Logic extends separation logic and Hyper Hoare Logic with a hyper separating conjunction to support arbitrary quantifier alternation for hyperproperties over heap programs, with a soundness proof in Isabelle/HOL.
A Rocq formalization defines simplicial Lagrange finite elements as records with geometric data, polynomial approximations, and unisolvence proofs for any dimension and polynomial degree.
A sound and complete unification procedure is given for deterministic higher-order patterns that allows infinite minimal complete sets of unifiers and leaves decidability open.
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.
-
Hyper Separation Logic (extended version)
Hyper Separation Logic extends separation logic and Hyper Hoare Logic with a hyper separating conjunction to support arbitrary quantifier alternation for hyperproperties over heap programs, with a soundness proof in Isabelle/HOL.
-
A Rocq Formalization of Simplicial Lagrange Finite Elements
A Rocq formalization defines simplicial Lagrange finite elements as records with geometric data, polynomial approximations, and unisolvence proofs for any dimension and polynomial degree.
-
Unification of Deterministic Higher-Order Patterns (Full Version)
A sound and complete unification procedure is given for deterministic higher-order patterns that allows infinite minimal complete sets of unifiers and leaves decidability open.
-
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.