Noninterference for Operating System Kernels. - Toby C. Murray; Daniel Matichuk; Matthew Brassil; Peter Gammie; Gerwin Klein (CPP, 2012)

Extensible Specifications for Automatic Re-use of Specifications and Proofs. - Daniel Matichuk; Toby C. Murray (SEFM, 2012)

Automatic Function Annotations for Hoare Logic - Daniel Matichuk (SSV, 2012)

seL4: From General Purpose to a Proof of Information Flow Enforcement. - Toby C. Murray; Daniel Matichuk; Matthew Brassil; Peter Gammie; Timothy Bourke; Sean Seefried; Corey Lewis; Xin Gao; Gerwin Klein (IEEE Symposium on Security and Privacy, 2013)

An Isabelle Proof Method Language. - Daniel Matichuk; Makarius Wenzel; Toby C. Murray (ITP, 2014)

Empirical Study Towards a Leading Indicator for Cost of Formal Software Verification. - Daniel Matichuk; Toby C. Murray; June Andronick; D. Ross Jeffery; Gerwin Klein; Mark Staples (ICSE (1), 2015)

Mining the Archive of Formal Proofs. - Jasmin Christian Blanchette; Max W. Haslbeck; Daniel Matichuk; Tobias Nipkow (CICM, 2015)

Proof of OS Scheduling Behavior in the Presence of Interrupt-Induced Concurrency. - June Andronick; Corey Lewis; Daniel Matichuk; Carroll Morgan; Christine Rizkallah (ITP, 2016)

Finite Machine Word Library. - Joel Beeren; Matthew Fernandez; Xin Gao; Gerwin Klein; Rafal Kolanski; Japheth Lim; Corey Lewis; Daniel Matichuk; Thomas Sewell (Arch. Formal Proofs, 2016)

Eisbach: A Proof Method Language for Isabelle. - Daniel Matichuk; Toby C. Murray; Makarius Wenzel (J. Autom. Reason., 2016)

Modular Verification Scopes via Export Sets and Translucent Exports. - K. Rustan M. Leino; Daniel Matichuk (Principled Software Development, 2018)

Automation for Proof Engineering: Machine-Checked Proofs At Scale. - Daniel Matichuk (2018)

Macaw: A Machine Code Toolbox for the Busy Binary Analyst. - Ryan G. Scott; Brett Boston; Benjamin Davis; Iavor S. Diatchki; Mike Dodds; Joe Hendrix; Daniel Matichuk; Kevin Quick; Tristan Ravitch; Valentin Robert; Benjamin Selfridge; Andrei Stefanescu; et al. (CoRR, 2024)