ÜBERSPARK : Enforcing Verifiable Object Abstractions for Automated Compositional Security Analysis of a Hypervisor

   Abstract