| seL4: from general purpose to a proof of information flow enforcement T Murray, D Matichuk, M Brassil, P Gammie, T Bourke, S Seefried, ... 2013 IEEE Symposium on Security and Privacy, 415-429, 2013 | 298 | 2013 |
| Noninterference for operating system kernels T Murray, D Matichuk, M Brassil, P Gammie, G Klein Certified Programs and Proofs: Second International Conference, CPP 2012 …, 2012 | 85 | 2012 |
| Eisbach: A proof method language for Isabelle D Matichuk, T Murray, M Wenzel Journal of Automated Reasoning 56 (3), 261-282, 2016 | 71 | 2016 |
| Mining the archive of formal proofs JC Blanchette, M Haslbeck, D Matichuk, T Nipkow International Conference on Intelligent Computer Mathematics, 3-17, 2015 | 67 | 2015 |
| Empirical study towards a leading indicator for cost of formal software verification D Matichuk, T Murray, J Andronick, R Jeffery, G Klein, M Staples 2015 IEEE/ACM 37th IEEE International Conference on Software Engineering 1 …, 2015 | 34 | 2015 |
| An Isabelle proof method language D Matichuk, M Wenzel, T Murray Interactive Theorem Proving: 5th International Conference, ITP 2014, Held as …, 2014 | 29 | 2014 |
| Proof of OS scheduling behavior in the presence of interrupt-induced concurrency J Andronick, C Lewis, D Matichuk, C Morgan, C Rizkallah International Conference on Interactive Theorem Proving, 52-68, 2016 | 23 | 2016 |
| Provably trustworthy systems G Klein, J Andronick, G Keller, D Matichuk, T Murray, L O'Connor Philosophical Transactions of the Royal Society A: Mathematical, Physical …, 2017 | 18 | 2017 |
| Extensible specifications for automatic re-use of specifications and proofs D Matichuk, T Murray International Conference on Software Engineering and Formal Methods, 333-341, 2012 | 10 | 2012 |
| Finite Machine Word Library J Beeren, M Fernandez, X Gao, G Klein, R Kolanski, J Lim, C Lewis, ... Archive of Formal Proofs, 2016 | 8 | 2016 |
| The Eisbach user manual D Matichuk, M Wenzel, T Murray Isabelle Community 263, 2015 | 7 | 2015 |
| Modular verification scopes via export sets and translucent exports KRM Leino, D Matichuk Principled Software Development: Essays Dedicated to Arnd Poetzsch-Heffter …, 2018 | 6 | 2018 |
| Automatic Function Annotations for Hoare Logic D Matichuk arXiv preprint arXiv:1211.6188, 2012 | 2 | 2012 |
| Automation for Proof Engineering: Machine-Checked Proofs at Scale D Matichuk University of New South Wales, 2018 | 1 | 2018 |
Toby MurraySchool of Computing and Information Systems, University of MelbourneEmail verificata su unimelb.edu.au