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

DOI10.1007/S10817-009-9122-0MaRDI QIDQ835773zbMATH OpenOpenAlexFDO

Authors 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 verificationmemory-mapped devicesmicro-hypervisoroperating-system kernelvirtual memory

Mathematics Subject Classification ID

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

Recommendations

• Formal verification of a C-like memory model and its uses for verifying program transformations
• scientific article; zbMATH DE number 1949622
• Semi-formal verification of memory systems by symbolic simulation
• Effective Program Verification for Relaxed Memory Models
• Correct Hardware Design and Verification Methods
• Effective abstractions for verification under relaxed memory models
• Effective Abstractions for Verification under Relaxed Memory Models

Cites work

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

Cited in

(21)

• Effective Abstractions for Verification under Relaxed Memory Models
• Formal reasoning under cached address translation
• Formal Pervasive Verification of a Paging Mechanism
• Correct Hardware Design and Verification Methods
• Balancing the load. Leveraging a semantics stack for systems verification
• Formal verification of a C-like memory model and its uses for verifying program transformations
• Formal stystems specification. The RPC-memory specification case study
• A Unified Memory Model for Pointers
• System-level non-interference of constant-time cryptography. I: Model
• Operating system task management requirements layer modeling and verification based on Coq
• Mechanising a formal model of flash memory
• Toward compositional verification of interruptible OS kernels and device drivers
• Physical addressing on real hardware in Isabelle/HOL
• Program verification in the presence of cached address translation
• Operating system verification---an overview
• Compositional verification of a baby virtual memory manager
• Parametric verification of address space separation
• Formally verified implementation of an idealized model of virtualization
• Correct Hardware Design and Verification Methods
• A verified specification of TLSF memory management allocator using state monads
• Types, Maps and Separation Logic

Describes a project that uses

Uses Software

• Kit
• PVS
• veriSoft

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

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