Formal memory models for the verification of low-level operating-system code

DOI10.1007/S10817-009-9122-0zbMath1191.68178OpenAlexW2104622601MaRDI QIDQ835773

Hendrik Tews, Marcus Völp, Tjark Weber

Publication date: 31 August 2009

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-009-9122-0

zbMATH Keywords

formal verificationvirtual memorymemory-mapped devicesmicro-hypervisoroperating-system kernel

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65) Theory of operating systems (68N25)

Related Items (2)

Types, Maps and Separation Logic ⋮ System-level non-interference of constant-time cryptography. I: Model

Uses Software

• veriSoft
• PVS
• Kit

Cites Work

• Operating system verification---an overview
• Types, bytes, and separation logic
• Specification and verification of the UCLA Unix security kernel
• A Unified Memory Model for Pointers
• Logic for Programming, Artificial Intelligence, and Reasoning

This page was built for publication: Formal memory models for the verification of low-level operating-system code