Integration of a Software Model Checker into Isabelle. - Matthias Daum 001; Stefan Maus; Norbert Schirmer; Mohamed Nassim Seghir (LPAR, 2005)

Model Stack for the Pervasive Verification of a Microkernel-based Operating System. - Matthias Daum 001; Jan Dörrenbächer; Sebastian Bogan (VERIFY, 2008)

A Verification Approach for System-Level Concurrent Programs. - Matthias Daum 001; Jan Dörrenbächer; Mareike Schmidt; Burkhart Wolff (VSTTE, 2008)

Implementation Correctness of a Real-Time Operating System. - Matthias Daum 001; Norbert Schirmer; Mareike Schmidt (SEFM, 2009)

Proving Fairness and Implementation Correctness of a Microkernel Scheduler. - Matthias Daum 001; Jan Dörrenbächer; Burkhart Wolff (J. Autom. Reason., 2009)

From Operating-System Correctness to Pervasively Verified Applications. - Matthias Daum 001; Norbert Schirmer; Mareike Schmidt (IFM, 2010)

On the formal foundation of a verification approach for system-level concurrent programs. - Matthias Daum 001 (2010)

Challenges and Experiences in Managing Large-Scale Proofs. - Timothy Bourke; Matthias Daum 001; Gerwin Klein; Rafal Kolanski (AISC/MKM/Calculemus, 2012)

Concerned with the unprivileged: user programs in kernel refinement. - Matthias Daum 001; Nelson Billing; Gerwin Klein (Formal Aspects Comput., 2014)