ÆÈ·Î¿ì
Michael Norrish
Michael Norrish
anu.edu.auÀÇ À̸ÞÀÏ È®ÀÎµÊ - ȨÆäÀÌÁö
Á¦¸ñ
Àοë
Àοë
¿¬µµ
seL4: Formal verification of an OS kernel
G Klein, K Elphinstone, G Heiser, J Andronick, D Cock, P Derrin, ...
Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles ¡¦, 2009
27032009
CakeML: a verified implementation of ML
R Kumar, MO Myreen, M Norrish, S Owens
ACM SIGPLAN Notices 49 (1), 179-191, 2014
4812014
A brief overview of HOL4
K Slind, M Norrish
International Conference on Theorem Proving in Higher Order Logics, 28-32, 2008
4122008
C formalised in HOL
M Norrish
University of Cambridge, Computer Laboratory, 1998
2871998
Types, bytes, and separation logic
H Tuch, G Klein, M Norrish
Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of ¡¦, 2007
2362007
Rigorous specification and conformance testing techniques for network protocols, as applied to TCP, UDP, and Sockets
S Bishop, M Fairbairn, M Norrish, P Sewell, M Smith, K Wansbrough
Proceedings of the 2005 conference on Applications, technologies ¡¦, 2005
1312005
The PROSPER toolkit
LA Dennis, G Collins, M Norrish, R Boulton, K Slind, G Robinson, ...
Tools and Algorithms for the Construction and Analysis of Systems: 6th ¡¦, 2000
1122000
A new verified compiler backend for CakeML
YK Tan, MO Myreen, R Kumar, A Fox, S Owens, M Norrish
Proceedings of the 21st ACM SIGPLAN International Conference on Functional ¡¦, 2016
972016
Barendregt¡¯s variable convention in rule inductions
C Urban, S Berghofer, M Norrish
Automated Deduction–CADE-21: 21st International Conference on Automated ¡¦, 2007
852007
The verified CakeML compiler backend
YK Tan, MO Myreen, R Kumar, A Fox, S Owens, M Norrish
Journal of Functional Programming 29, e2, 2019
722019
Engineering with logic: HOL specification and symbolic-evaluation testing for TCP implementations
S Bishop, M Fairbairn, M Norrish, P Sewell, M Smith, K Wansbrough
Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of ¡¦, 2006
682006
Mind the gap: A verification framework for low-level C
S Winwood, G Klein, T Sewell, J Andronick, D Cock, M Norrish
Theorem Proving in Higher Order Logics: 22nd International Conference ¡¦, 2009
632009
Seed selection for successful fuzzing
A Herrera, H Gunadi, S Magrath, M Norrish, M Payer, AL Hosking
Proceedings of the 30th ACM SIGSOFT international symposium on software ¡¦, 2021
582021
TacticToe: learning to prove with tactics
T Gauthier, C Kaliszyk, J Urban, R Kumar, M Norrish
Journal of Automated Reasoning 65, 257-286, 2021
55*2021
Verified characteristic formulae for CakeML
A Guéneau, MO Myreen, R Kumar, M Norrish
Programming Languages and Systems: 26th European Symposium on Programming ¡¦, 2017
532017
Mechanised computability theory
M Norrish
Interactive Theorem Proving: Second International Conference, ITP 2011, Berg ¡¦, 2011
442011
Recursive function definition for types with binders
M Norrish
International Conference on Theorem Proving in Higher Order Logics, 241-256, 2004
392004
Deterministic expressions in C
M Norrish
European Symposium on Programming, 147-161, 1999
381999
Verified compilation on a verified processor
A Lööw, R Kumar, YK Tan, MO Myreen, M Norrish, O Abrahamsson, A Fox
Proceedings of the 40th ACM SIGPLAN Conference on Programming Language ¡¦, 2019
362019
Verified, executable parsing
A Barthwal, M Norrish
Programming Languages and Systems: 18th European Symposium on Programming ¡¦, 2009
362009
ÇöÀç ½Ã½ºÅÛÀÌ ÀÛµ¿µÇÁö ¾Ê½À´Ï´Ù. ³ªÁß¿¡ ´Ù½Ã ½ÃµµÇØ ÁÖ¼¼¿ä.
ÇмúÀÚ·á 1–20