Mechanically Checked Proofs of Kernel Specification
No abstract available.
Related papers
- Mechanized verification of preemptive OS kernels (invited talk) CPP 2017
- McTT: A Verified Kernel for a Proof Assistant ICFP 2025
- Checking Data-Race Freedom of GPU Kernels, Compositionally CAV 2021
- End-to-End Mechanized Proof of an eBPF Virtual Machine for Micro-controllers CAV 2022
- End-to-End Mechanized Proof of a JIT-Accelerated eBPF Virtual Machine for IoT CAV 2024
- Inferring frame conditions with static correlation analysis POPL 2019
- Pattern Matching in AI Compilers and Its Formalization CGO 2025
- Coq Coq correct! verification of type checking and erasure for Coq, in Coq POPL 2020