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

DOI10.1007/S10817-009-9122-0zbMATH Open1191.68178OpenAlexW2104622601MaRDI QIDQ835773FDOQ835773

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

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

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)

Cites Work

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

Cited In (21)

• 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
• Compositional verification of a baby virtual memory manager
• Operating system verification---an overview
• 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
• Effective Abstractions for Verification under Relaxed Memory Models

Uses Software

• veriSoft
• PVS
• Kit

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)