Combining Mechanized Proofs and Model-Based Testing in
the Formal Analysis of a Hypervisor, published in the
proceedings of FM2016 in LNCS 9995, pages 69-84.
Done together with the FireEye Formal Methods Team (Hanno, Juan, Ulrich,
Yoichi, Cesar, Keiko,
Jorge and Thomas)
and Jacek. copy paper: [pdf]
copy slides [pdf]
Solving Operating-Systems Problems with Probabilistic
Model Checking, presentation for the
resilience path of cfaed (the Center for Advancing Electronics
Dresden), TU Dresden, Mai 3rd, 2013
[copy slides]