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

(13)

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

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)