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
9 Pith papers cite this work. Polarity classification is still indexing.
9
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 multi-agent framework called AutoformBot autoformalized 26 textbooks spanning analysis, algebra, topology, combinatorics and probability into a verified Lean 4 library of 45k declarations, demonstrating scalable formalization of graduate math.
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.
Forge pipeline combines LLM code generation with MDE transformations to produce verifiable artifacts in Dafny, CSP, and Isabelle, iterating on failures to generate standards-relevant evidence for Java code.
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.
Introduces Abduction Prover that constructs proof scripts in Isabelle/HOL by identifying useful conjectures via abductive reasoning.
citing papers explorer
-
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.
-
Formal-Method-Guided Vibe Coding: Closing the Verification Loop on AI-Generated Safety-Critical Software Through Model-Driven Engineering
Forge pipeline combines LLM code generation with MDE transformations to produce verifiable artifacts in Dafny, CSP, and Isabelle, iterating on failures to generate standards-relevant evidence for Java code.
-
Abduction Prover in Isabelle/HOL
Introduces Abduction Prover that constructs proof scripts in Isabelle/HOL by identifying useful conjectures via abductive reasoning.