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
- Connecting higher-order separation logic to a first-order outside world
- 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
- Bar induction is compatible with constructive type theory
- ANF preserves dependent types up to extensional equality
This page was built for software: CertiKOS
