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
-
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.
-
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.