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
- TRX
- CompCert
- Vellvm
- seL4
- ARMor
- CertiCoq
- TIL
- HoTTSQL
- Barrelfish
- Kami
- Q*cert
- SEQUEL
- SQLCert
- CacheAudit
- 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
