CertiKOS
From MaRDI portal
Cited in
(24)- Toward compositional verification of interruptible OS kernels and device drivers
- Physical addressing on real hardware in Isabelle/HOL
- A Coq formalisation of SQL's execution engines
- Program verification in the presence of cached address translation
- TRX
- CompCert
- Formal reasoning under cached address translation
- Formal verification of integrity-preserving countermeasures against cache storage side-channels
- Vellvm
- seL4
- ARMor
- TIL
- CertiCoq
- HoTTSQL
- Kami
- Barrelfish
- Q*cert
- SQLCert
- SEQUEL
- CacheAudit
- Reasoning about Translation Lookaside Buffers
- Connecting higher-order separation logic to a first-order outside world
- ANF preserves dependent types up to extensional equality
- Bar induction is compatible with constructive type theory
This page was built for software: CertiKOS
