Skip to main content

Daniel Matichuk

Daniel Matichuk
Research Engineer

Research Interests

Daniel is interested in interactive theorem provers and proof automation. His current work is in increasing the scalability and maintainability of formal machine-checked proofs through refactoring.

Contact Details

Email:Daniel.Matichuk@data61.csiro.au

More contact information is available at the Contact page.

Photo of Daniel Matichuk

Publication List

Projects

Current

Past

Qualifications

Daniel has a Bachelor of Science (Honors Computing Science) from the University of Alberta.

Publications

Best Papers

Abstract
Slides
PDF Toby Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Timothy Bourke, Sean Seefried, Corey Lewis, Xin Gao and Gerwin Klein
seL4: From general purpose to a proof of information flow enforcement
IEEE Symposium on Security and Privacy, pp. 415-429, San Francisco, CA, May, 2013


Data61 Papers

2017

Abstract PDF Gerwin Klein, June Andronick, Gabriele Keller, Daniel Matichuk and Toby Murray
Provably trustworthy systems
Philosophical Transactions of the Royal SocietyA, Volume 375, pp. 1-23, September, 2017

2016

Abstract PDF June Andronick, Corey Lewis, Daniel Matichuk, Carroll Morgan and Christine Rizkallah
Proof of OS scheduling behavior in the presence of interrupt-induced concurrency
International Conference on Interactive Theorem Proving, pp. 52-68, Nancy, France, August, 2016

NICTA Papers

2016

Abstract PDF Daniel Matichuk, Toby Murray and Makarius Wenzel
Eisbach: A proof method language for isabelle
Journal of Automated Reasoning, Volume 56, Number 3, pp. 261-282, March, 2016

2015

Abstract PDF Jasmin Blanchette, Maximilian Haslbeck, Daniel Matichuk and Tobias Nipkow
Mining the archive of formal proofs
Conference on Intelligent Computer Mathematics, pp. 3-17, Washington DC, USA, July, 2015
Abstract PDF Daniel Matichuk, Toby Murray, June Andronick, Ross Jeffery, Gerwin Klein and Mark Staples
Empirical study towards a leading indicator for cost of formal software verification
International Conference on Software Engineering, pp. 11, Firenze, Italy, February, 2015

2014

Abstract PDF Daniel Matichuk, Makarius Wenzel and Toby Murray
An Isabelle proof method language
International Conference on Interactive Theorem Proving, pp. 390-405, Vienna, Austria, July, 2014

2013

Abstract
Slides
PDF Toby Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Timothy Bourke, Sean Seefried, Corey Lewis, Xin Gao and Gerwin Klein
seL4: From general purpose to a proof of information flow enforcement
IEEE Symposium on Security and Privacy, pp. 415-429, San Francisco, CA, May, 2013

2012

Abstract PDF Daniel Matichuk and Toby Murray
Extensible specifications for automatic re-use of specifications and proofs
10th International Conference on Software Engineering and Formal Methods, pp. 8, Thessaloniki, Greece, December, 2012
Abstract PDF Toby Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie and Gerwin Klein
Noninterference for operating system kernels
International Conference on Certified Programs and Proofs, pp. 126-142, Kyoto, Japan, December, 2012
Abstract PDF Daniel Matichuk
Automatic function annotations for hoare logic
Systems Software Verification, pp. 10, Sydney, Australia, November, 2012

Served by Apache on Linux on seL4.