Machine Assisted Proof of ARMv7 Instruction Level Isolation Properties
No abstract available.
Related papers
- End-to-End Mechanized Proof of an eBPF Virtual Machine for Micro-controllers CAV 2022
- Promising Compilation to ARMv8 POP ECOOP 2017
- A Formal Framework for the Derivation of Machine-Specific Optimizers TOPLAS 1983
- Virtual timeline: a formal abstraction for verifying preemptive schedulers with temporal isolation POPL 2020
- Isolation and Analysis of Optimization Errors PLDI 1993
- Reasoning about Weak Isolation Levels in Separation Logic ICFP 2025
- Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4 TACAS 2025
- Certified undecidability of intuitionistic linear logic via binary stack machines and minsky machines CPP 2019