@misc(AMD,
 author       = "{Advanced Micro Devices}",
 year         = "2005",
 title        = "AMD64 virtualization: Secure virtual machine architecture reference manual",
 howpublished = "AMD Publication no. 33047 rev. 3.01",
)
@misc(Alkassar,
 author       = "E. Alkassar and W. Paul",
 year         = "2008",
 title        = "On the verification of a "baby" hypervisor for a RISC machine; draft 0",
 howpublished = "available online",
)
@inproceedings(XEN,
 author       = "Paul Barham and Boris Dragovic and Keir Fraser and Steven Hand and Tim Harris and Alex Ho and Rolf Neugebauer and Ian Pratt and Andrew Warfield",
 year         = "2003",
 title        = "Xen and the art of virtualization",
 booktitle    = "SOSP '03: Proceedings of the Nineteenth {ACM} Symposium on Operating Systems Principles",
 publisher    = "ACM",
 address      = "New York, NY, USA",
 pages        = "164--177",
 doi          = "10.1145/945445.945462",
)
@article(CLIStack,
 author       = "William R. Bevier and Warren A. {Hunt, Jr.} and J S. Moore and William D. Young",
 year         = "1989",
 title        = "An Approach to System Verification",
 journal      = "Journal of Automated Reasoning",
 volume       = "5",
 number       = "4",
 pages        = "411--428",
)
@article(VAMP,
 author       = "Sven Beyer and Christian Jacobi and Daniel Kroning and Dirk Leinenbach and Wolfgang J. Paul",
 year         = "2006",
 title        = "Putting it all together: Formal verification of the {VAMP}",
 journal      = "International Journal on Software Tools Technology Transfer",
 volume       = "8",
 number       = "4",
 pages        = "411--430",
 doi          = "10.1007/s10009-006-0204-6",
)
@book(BryantOHallaron,
 author       = "Randal E. Bryant and David O'Hallaron",
 year         = "2003",
 title        = "Computer Systems: A Programmer's Perspective",
 publisher    = "Prentice-Hall",
 address      = "Upper Saddle River, N.J.",
)
@inproceedings(VCC,
 author       = "Ernie Cohen and Markus Dahlweid and Mark Hillebrand and Dirk Leinenbach and Michal Moskal and Thomas Santen and Wolfram Schulte and Stephan Tobies",
 year         = "2009",
 title        = "VCC: A Practical System for Verifying Concurrent C",
 booktitle    = "Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics",
 series       = "TPHOLs '09",
 publisher    = "Springer-Verlag",
 address      = "Berlin, Heidelberg",
 pages        = "23--42",
 doi          = "{10.1007/978-3-642-03359-9_2}",
)
@techreport(PXE,
 author       = "Intel Corporation",
 year         = "1999",
 title        = "Preboot Execution Environment, Verion 2.1",
 type         = "Technical Report",
 institution  = "Intel Corporation",
)
@misc(Franklin08,
 author       = "Jason Franklin and Arvind Seshadri and Ning Qu and Sagar Chaki and Anupam Datta",
 year         = "2008",
 title        = "Attacking, Repairing, and Verifying SecVisor: A Retrospective on the Security of a Hypervisor",
 howpublished = "submitted to 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI'08)",
)
@inproceedings(HardinSmithYoung,
 author       = "David S. Hardin and Eric W. Smith and William D. Young",
 year         = "2006",
 title        = "A Robust Machine Code Proof Framework for Highly Secure Applications",
 booktitle    = "Proceeding of the 2006 International Workshop on ACL2",
 publisher    = "ACM",
)
@book(HessNewman,
 author       = "Kenneth Hess and Amy Newman",
 year         = "2010",
 title        = "Practical Virtualization Solutions",
 publisher    = "Pearson Education",
 address      = "Boston",
)
@mastersthesis(Hoffmann,
 author       = "Sarah Hoffmann",
 year         = "2003",
 title        = "Formalising {PC} Hardware: A Model of the x86 Architecture",
 school       = "Technische Universitat Dresden",
)
@misc(Intel,
 author       = "{Intel Corporation}",
 year         = "2006",
 title        = "LaGrande technology preliminary architecture specification",
 howpublished = "Intel Publication no. D52212",
)
@misc(JOS,
 year         = "2006",
 title        = "{JOS Operating System}",
 howpublished = "\burl {http://pdos.csail.mit.edu/6.828/2006/overview.html}",
)
@book(ACL2Book,
 author       = "M. Kaufmann and P. Manolios and J Moore",
 year         = "2000",
 title        = "Computer-Aided Reasoning: An Approach",
 publisher    = "Kluwer Academic Press",
 address      = "Boston",
 doi          = "10.1007/978-1-4615-4449-4",
)
@inproceedings(seL4,
 author       = "Gerwin Klein and Kevin Elphinstone and Gernot Heiser and June Andronick and David Cock and Philip Derrin and Dhammika Elkaduwe and Kai Engelhardt and Rafal Kolanski and Michael Norrish and Thomas Sewell and Harvey Tuch and Simon Winwood",
 year         = "2009",
 title        = "seL4: formal verification of an OS kernel",
 booktitle    = "Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles",
 series       = "SOSP '09",
 publisher    = "ACM",
 address      = "New York",
 pages        = "207--220",
 doi          = "10.1145/1743546.1743574",
)
@misc(KVM,
 author       = "KVM",
 year         = "2011",
 title        = "Kernel Based Virtual Machine",
 howpublished = "\burl {www.linux-kvm.org/page/Main_Page}",
)
@inproceedings(Leslie,
 author       = "Rebekah Leslie and Levent Erk\"ok and Flemming Andersen",
 year         = "2007",
 title        = "Formalizing Information Flow in a {Haskell} Hypervisor",
 booktitle    = "Microkernels and Embedded Systems Workshop, MIKES'07",
)
@inproceedings(ACL2cutpoints,
 author       = "J. Matthews and J S. Moore and S. Ray and D. Vroon",
 year         = "2006",
 title        = "{Verification Condition Generation Via Theorem Proving}",
 editor       = "M. Hermann and A. Voronkov",
 booktitle    = "{Proceedings of the $13$th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2006)}",
 series       = "LNCS",
 volume       = "4246",
 publisher    = "Springer",
 address      = "{Phnom Penh, Cambodia}",
 pages        = "362--376",
 doi          = "10.1.1.101.503",
)
@article(McDermott08,
 author       = "J. McDermott and J. Kirby and B. Montrose and T. Johnson and M. Kang",
 year         = "2008",
 title        = "Re-engineering Xen internals for higher-assurance security",
 journal      = "Information Security Technical Report",
 volume       = "13",
 number       = "1",
 pages        = "17--24",
 doi          = "10.1016/j.istr.2008.01.001",
)
@inproceedings(XenonPolicy,
 author       = "John McDermott and Leo Freitas",
 year         = "2008",
 title        = "A formal security policy for {X}enon",
 booktitle    = "FMSE '08: Proceedings of the 6th ACM workshop on Formal methods in security engineering",
 publisher    = "ACM",
 address      = "New York, NY, USA",
 pages        = "43--52",
 doi          = "10.1145/1456396.1456401",
)
@inproceedings(Moore-cutpoints,
 author       = "J S. Moore",
 year         = "2003",
 title        = "Inductive Assertions and Operational Semantics",
 booktitle    = "CHARME 2003, Volume 2860 of LNCS",
 publisher    = "Springer-Verlag",
 pages        = "289--303",
 doi          = "10.1007/s10009-005-0180-2",
)
@phdthesis(Raydissertation,
 author       = "Sandip Ray",
 year         = "2005",
 title        = "Using Theorem Proving and Algorithmic Design Procedures for Large-Scale System Verification",
 school       = "University of Texas at Austin",
)
@inproceedings(Roscoe,
 author       = "A. Roscoe and J. Woodcock and L. Wulf",
 year         = "1997",
 title        = "Non-interference through nondeterminism",
 booktitle    = "Proceedings ESORICS",
 pages        = "33--52",
)
@inproceedings(SecVisor,
 author       = "Arvind Seshadri and Mark Luk and Ning Qu and Adrian Perrig",
 year         = "2007",
 title        = "SecVisor: A Tiny Hypervisor to Provide Lifetime Kernel Code Integrity for Commodity {OSes}",
 booktitle    = "SOSP '07: Proceedings of Twenty-first ACM SIGOPS Symposium on Operating Systems Principles",
 publisher    = "ACM",
 pages        = "335--350",
 doi          = "10.1145/1323293.1294294",
)
@book(SmithNair,
 author       = "James E. Smith and Ravi Nair",
 year         = "2005",
 title        = "Virtual Machines: Versatile Platforms for Systems and Processes",
 publisher    = "Morgan Kaufmann",
 address      = "Boston",
)
@techreport(Nova,
 author       = "Hendrik Tews and Bart Jacobs and Erik Poll and Marko van Eekelen and Peter van Rossum",
 year         = "2005",
 title        = "Specification and Verification of the {Nova} microhypervisor",
 type         = "Project Robin deliverable",
 number       = "D.6",
 institution  = "Radboud University Nijmegen",
)
@misc(Verisoft,
 author       = "Verisoft",
 year         = "2008",
 title        = "Verisoft Repository",
 howpublished = "\burl {www.verisoft.de/VerisoftRepository.html}",
)