CertiKOS
From MaRDI portal
Software:33310
swMATH21503MaRDI QIDQ33310FDOQ33310
Author name not available (Why is that?)
Cited In (10)
- Formal reasoning under cached address translation
- Formal verification of integrity-preserving countermeasures against cache storage side-channels
- Bar Induction is Compatible with Constructive Type Theory
- Reasoning about Translation Lookaside Buffers
- Toward compositional verification of interruptible OS kernels and device drivers
- A Coq formalisation of SQL's execution engines
- Physical addressing on real hardware in Isabelle/HOL
- Program verification in the presence of cached address translation
- Connecting Higher-Order Separation Logic to a First-Order Outside World
- ANF preserves dependent types up to extensional equality
This page was built for software: CertiKOS
