Using XCAP to Certify Realistic Systems Code: Machine Context Management

DOI10.1007/978-3-540-74591-4_15zbMath1144.68325OpenAlexW1937179622MaRDI QIDQ3523175

Zhong Shao, Dachuan Yu, Zhaozhong Ni

Publication date: 2 September 2008

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-74591-4_15

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (6)

Certifying low-level programs with hardware interrupts and preemptive threads ⋮ Proving fairness and implementation correctness of a microkernel scheduler ⋮ Balancing the load. Leveraging a semantics stack for systems verification ⋮ Improved Tool Support for Machine-Code Decompilation in HOL4 ⋮ Function extraction ⋮ Operating system verification---an overview

Uses Software

• Coq

This page was built for publication: Using XCAP to Certify Realistic Systems Code: Machine Context Management