Verified Process-Context Switch for C-Programmed Kernels. - Artem Starostin; Alexandra Tsyban (VSTTE, 2008)

CVM - A Verified Framework for Microkernel Programmers. - Thomas In der Rieden; Alexandra Tsyban (SSV, 2008)

Correct Microkernel Primitives. - Artem Starostin; Alexandra Tsyban (SSV, 2008)

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)

Balancing the Load. - Eyad Alkassar; Mark A. Hillebrand; Dirk Leinenbach; Norbert Schirmer; Artem Starostin; Alexandra Tsyban (J. Autom. Reason., 2009)

Pervasive Verification of an OS Microkernel - Inline Assembly, Memory Consumption, Concurrent Devices. - Eyad Alkassar; Wolfgang J. Paul; Artem Starostin; Alexandra Tsyban (VSTTE, 2010)