Formal Pervasive Verification of a Paging Mechanism

DOI10.1007/978-3-540-78800-3_9MaRDI QIDQ5458324zbMATH OpenOpenAlexFDO

Authors Eyad Alkassar, Norbert W. Schirmer, Artem Starostin

Publication date 11 April 2008

Published in Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-78800-3_9

Mathematics Subject Classification ID

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

Recommendations

• Correct Hardware Design and Verification Methods
• Formal memory models for the verification of low-level operating-system code
• A Unified Memory Model for Pointers
• Operating system verification---an overview
• Balancing the load. Leveraging a semantics stack for systems verification

Cited in

(12)

• Correct Hardware Design and Verification Methods
• Balancing the load. Leveraging a semantics stack for systems verification
• Proving the correctness of client/server software
• The Isabelle Framework
• A Unified Memory Model for Pointers
• Verifying software emulation of an unsupported hardware instruction
• Operating system verification---an overview
• Compositional verification of a baby virtual memory manager
• Parametric verification of address space separation
• Proving fairness and implementation correctness of a microkernel scheduler
• A verified specification of TLSF memory management allocator using state monads
• Types, Maps and Separation Logic

This page was built for publication: Formal Pervasive Verification of a Paging Mechanism

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