CertiKOS
From MaRDI portal
swMATH21503MaRDI QIDQ33310FDOQ33310
Author name not available (Why is that?)
Official website: https://dl.acm.org/citation.cfm?id=3026928
Cited In (24)
- 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
- TRX
- CompCert
- Vellvm
- seL4
- 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
- ARMor
- CertiCoq
- TIL
- HoTTSQL
- Barrelfish
- Kami
- Q*cert
- SEQUEL
- SQLCert
- CacheAudit
- Bar induction is compatible with constructive type theory
- ANF preserves dependent types up to extensional equality
This page was built for software: CertiKOS
