On PDG-based noninterference and its modular proof. - Daniel Wasserrab; Denis Lohner; Gregor Snelting (PLAS, 2009)

Proving Information Flow Noninterference by Reusing a Machine-Checked Correctness Proof for Slicing. - Daniel Wasserrab; Denis Lohner (VERIFY@IJCAR, 2010)

Verified construction of static single assignment form. - Sebastian Buchwald; Denis Lohner; Sebastian Ullrich 002 (CC, 2016)

The meta theory of the Incredible Proof Machine. - Joachim Breitner; Denis Lohner (Arch. Formal Proofs, 2016)

Verified Construction of Static Single Assignment Form. - Sebastian Ullrich 002; Denis Lohner (Arch. Formal Proofs, 2016)

Minimal Static Single Assignment Form. - Max Wagner; Denis Lohner (Arch. Formal Proofs, 2017)

Illi Isabellistes Se Custodes Egregios Praestabant. - Simon Bischof; Joachim Breitner; Denis Lohner; Gregor Snelting (Principled Software Development, 2018)