CertiKOS
From MaRDI portal
Software:33310
No author found.
Related Items (10)
Connecting Higher-Order Separation Logic to a First-Order Outside World ⋮ ANF preserves dependent types up to extensional equality ⋮ Toward compositional verification of interruptible OS kernels and device drivers ⋮ Formal reasoning under cached address translation ⋮ Reasoning about Translation Lookaside Buffers ⋮ 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 ⋮ Formal verification of integrity-preserving countermeasures against cache storage side-channels ⋮ Bar Induction is Compatible with Constructive Type Theory
This page was built for software: CertiKOS
