Pages that link to "Item:Q3543657"
From MaRDI portal
The following pages link to Secure Microkernels, State Monads and Scalable Refinement (Q3543657):
Displaying 12 items.
- Eisbach: a proof method language for Isabelle (Q287365) (← links)
- Concerned with the unprivileged: user programs in kernel refinement (Q736848) (← links)
- Proving fairness and implementation correctness of a microkernel scheduler (Q835766) (← links)
- Operating system verification---an overview (Q1040002) (← links)
- An Isabelle/HOL formalisation of the SPARC instruction set architecture and the TSO memory model (Q2031429) (← links)
- A Framework for the Automatic Formal Verification of Refinement from Cogent to C (Q2829268) (← links)
- seL4 Enforces Integrity (Q3088017) (← links)
- A Hoare Logic for the State Monad (Q3183544) (← links)
- A monadic analysis of information flow security with mutable state (Q4676158) (← links)
- Cogent: uniqueness types and certifying compilation (Q5019022) (← links)
- A verified specification of TLSF memory management allocator using state monads (Q6535916) (← links)
- SSCalc: a calculus for Solidity smart contracts (Q6550597) (← links)