Verification

[Google Scholar]

Notes:
Papers:
  • Automated verification of a small hypervisor [alkassar:vstte:2010]
  • Combining mechanized proofs and model-based testing in the formal analysis of a hypervisor [becker:fm:2016]
  • A case study on formal verification of the Anaxagoros hypervisor paging system with Frama-C [blanchard:fmics:2015]
  • An automata-based framework for verification and bug hunting in quantum circuits [chen:pldi:2023]
  • Local verification of global invariants in concurrent programs [cohen:cav:2010]
  • Machine code verification of a tiny ARM hypervisor [dam:trusted:2013]
  • Attacking, repairing, and verifying SecVisor: A retrospective on the security of a hypervisor [franklin:cmu:2008]
  • CertiKOS: An extensible architecture for building certified concurrent OS Kernels [gu:osdi:2016]
  • SeL4: Formal verification of an OS kernel [klein:sosp:2009]
  • CryptOpt: Verified compilation with randomized program search for cryptographic primitives [kuepper:pldi:2023]
  • Design, implementation and verification of an extensible and modular hypervisor framework [vasudevan:secpriv:2013]
  • überSpark: Enforcing verifiable object abstractions for automated compositional security analysis of a hypervisor [vasudevan:usenix:2016]