A case study on formal verification of the Anaxagoros hypervisor paging system with Frama-C

Allan Blanchard, Nikolai Kosmatov, Matthieu Lemerre, Frédéric Loulergue
[doi] [Google Scholar] [DBLP] [Citeseer]

International Workshop on Formal Methods for Industrial Critical Systems
Springer
Pages 15-30
2015
Note(s): Frama-C verifier, Operating Systems, hypervisor, verification