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.
Isabelle/HOL: A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science
6 Pith papers cite this work. Polarity classification is still indexing.
6
Pith papers citing it
citation-role summary
background 4
citation-polarity summary
roles
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.
Relation algebras gain semantics for associative arrays that integrate with while-programs, enabling Isabelle/HOL proofs of correctness for disjoint-set forest implementations using union-by-rank and path compression, splitting or halving.
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.
-
Relation-Algebraic Verification of Disjoint-Set Forests
Relation algebras gain semantics for associative arrays that integrate with while-programs, enabling Isabelle/HOL proofs of correctness for disjoint-set forest implementations using union-by-rank and path compression, splitting or halving.