Invariants, Modularity, and Rights. - Ernie Cohen; Eyad Alkassar; Vladimir Boyarinov; Markus Dahlweid; Ulan Degenbaev; Mark A. Hillebrand; Bruno Langenstein; Dirk Leinenbach; Michal Moskal; Steven Obua; Wolfgang J. Paul; Hristo Pentchev; et al. (Ershov Memorial Conference, 2009)

Towards the Formal Verification of a Distributed Real-Time Automotive System. - Erik Endres; Christian Müller 009; Andrey Shadrin; Sergey Tverdyshev (NASA Formal Methods, 2010)

Completing the Automated Verification of a Small Hypervisor - Assembler Code Verification. - Wolfgang J. Paul; Sabine Schmaltz; Andrey Shadrin (SEFM, 2012)

Integrated Semantics of Intermediate-Language C and Macro-Assembler for Pervasive Formal Verification of Operating Systems and Hypervisors from VerisoftXT. - Sabine Schmaltz; Andrey Shadrin (VSTTE, 2012)

Mixed low- and high level programming language semantics and automated verification of a small hypervisor. - Andrey Shadrin (2012)