Concerned with the unprivileged: user programs in kernel refinement

DOI10.1007/S00165-014-0296-9zbMath1342.68079OpenAlexW2074245744MaRDI QIDQ736848

Nelson Billing, Matthias Daum, Gerwin Klein

Publication date: 5 August 2016

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00165-014-0296-9

zbMATH Keywords

microkernel correctnessrefinement prooftrustworthy systems

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (1)

Formal reasoning under cached address translation

Uses Software

• Isabelle/HOL
• VCC
• seL4

Cites Work

• Operating system verification---an overview
• seL4 Enforces Integrity
• Types, Maps and Separation Logic
• Secure Microkernels, State Monads and Scalable Refinement
• Data Refinement
• Noninterference for Operating System Kernels
• Compositional Verification of a Baby Virtual Memory Manager
• A Unified Memory Model for Pointers
• Logic for Programming, Artificial Intelligence, and Reasoning

This page was built for publication: Concerned with the unprivileged: user programs in kernel refinement