Formal Pervasive Verification of a Paging Mechanism

DOI10.1007/978-3-540-78800-3_9MaRDI QIDQ5458324zbMATHOpenAlexFDO

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

(11)

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

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)