Integrated semantics of intermediate-language C and macro-assembler for pervasive formal verification of operating systems and hypervisors from VerisoftXT

Sabine Schmaltz, Andrey Shadrin
[doi] [ISBN] [Google Scholar] [DBLP] [Citeseer]

Verified Software: Theories, Tools, Experiments
Springer Berlin Heidelberg
Berlin, Heidelberg
Pages 18-33
2012
Note(s): ISA specification, hypervisor, operating systems