Formalizing a JVML Verifier for Initialization in a Theorem Prover
Abstract elided by the publisher.
Related papers
- Verified heap theorem prover by paramodulation ICFP 2012
- Formally verified differential dynamic logic CPP 2017
- The Rocq-NN-Roll Prover: Soundly Verifying Hyperproperties of Neural Networks in Rocq CAV 2026
- A modular Isabelle framework for verifying saturation provers CPP 2021
- Formalizing the LLVM intermediate representation for verified program transformations POPL 2012
- Formalizing the One-Way to Hiding Theorem CPP 2025
- A Verified Compiler for Probability Density Functions ESOP 2015
- Compositional Neural-Cyber-Physical System Verification in the Interactive Theorem Prover of Your Choice ICFP 2026