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.
In: Clarke, E.M., Voronkov, A
11 Pith papers cite this work. Polarity classification is still indexing.
11
Pith papers citing it
citation-role summary
background 4
citation-polarity summary
roles
background 4polarities
background 4representative citing papers
ZipLex delivers the first verified lexer that is both linear-time and provably invertible between lexing and printing, using token-sequence abstractions, zippers, and a verified hash table in Stainless.
Caesar introduces a deductive verifier for probabilistic programs using the HeyVL language, Z3 SMT solving, and a probabilistic model-checking backend after five years of development.
Quantifier rewriting and array non-aliasing specifications in VerCors reduce verification time for data-level parallel programs by an average factor of 9.
A source-level interaction concept for interactive program verification, prototyped in KeY, improves user understanding of proof states and defect detection according to a user study.
The authors formally verify several minimax variants with alpha-beta and transposition tables in Dafny, proving one depth-limited negamax variant correct under a new witness-based criterion and exhibiting a counterexample for another.
Fuzz testing with the AValAnCHE prototype can uncover robustness issues in deductive verifiers such as VerCors and works across other similar tools.
AI agents can generate code in a capability-safe Scala dialect that statically prevents information leakage and malicious side effects while preserving task performance.
AutoRocq is an LLM agent that learns proofs on-the-fly by collaborating with the Rocq prover to verify programs on SV-COMP benchmarks and Linux kernel modules.
AutoQ 2.0 verifies quantum programs with classical control flow and successfully checks RUS algorithms instantly plus weak-measurement Grover search on 100 qubits in about 20 minutes.
SpecRL uses the fraction of negative tests rejected by candidate specifications as a reward signal in RL training to produce stronger and more verifiable formal specifications than prior methods.
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.
-
Formally Verified Linear-Time Invertible Lexing
ZipLex delivers the first verified lexer that is both linear-time and provably invertible between lexing and printing, using token-sequence abstractions, zippers, and a verified hash table in Stainless.
-
Caesar: A Deductive Verifier for Probabilistic Programs
Caesar introduces a deductive verifier for probabilistic programs using the HeyVL language, Z3 SMT solving, and a probabilistic model-checking backend after five years of development.
-
Scalable Deductive Verification of Data-Level Parallel Programs
Quantifier rewriting and array non-aliasing specifications in VerCors reduce verification time for data-level parallel programs by an average factor of 9.
-
A New Interaction Concept for Interactive and Autoactive Program Verification
A source-level interaction concept for interactive program verification, prototyped in KeY, improves user understanding of proof states and defect detection according to a user study.
-
Formal Verification of Minimax Algorithms
The authors formally verify several minimax variants with alpha-beta and transposition tables in Dafny, proving one depth-limited negamax variant correct under a new witness-based criterion and exhibiting a counterexample for another.
-
Crash-free Deductive Verifiers
Fuzz testing with the AValAnCHE prototype can uncover robustness issues in deductive verifiers such as VerCors and works across other similar tools.
-
Tracking Capabilities for Safer Agents
AI agents can generate code in a capability-safe Scala dialect that statically prevents information leakage and malicious side effects while preserving task performance.
-
Agentic Verification of Software Systems
AutoRocq is an LLM agent that learns proofs on-the-fly by collaborating with the Rocq prover to verify programs on SV-COMP benchmarks and Linux kernel modules.
-
AutoQ 2.0: From Verification of Quantum Circuits to Verification of Quantum Programs (Technical Report)
AutoQ 2.0 verifies quantum programs with classical control flow and successfully checks RUS algorithms instantly plus weak-measurement Grover search on 100 qubits in about 20 minutes.
-
Reinforcement Learning with Negative Tests as Completeness Signal for Formal Specification Synthesis
SpecRL uses the fraction of negative tests rejected by candidate specifications as a reward signal in RL training to produce stronger and more verifiable formal specifications than prior methods.