Verifying software emulation of an unsupported hardware instruction

DOI10.4230/LIPICS.ITP.2024.17MaRDI QIDQ6860015zbMATH OpenFDO

Authors Samuel Gruetter, Thomas Bourgeat, Adam Chlipala

Publication date 10 February 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.4230/LIPICS.ITP.2024.17

zbMATH Keywords

Coqsoftware verificationsoftware-hardware boundary

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• Compositional verification of a baby virtual memory manager
• Formal Pervasive Verification of a Paging Mechanism
• The verified CakeML compiler backend
• Toward compositional verification of interruptible OS kernels and device drivers

This page was built for publication: Verifying software emulation of an unsupported hardware instruction

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6860015)