| 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 | 2768 | 2009 |
| Comprehensive formal verification of an OS microkernel G Klein, J Andronick, K Elphinstone, T Murray, T Sewell, R Kolanski, ... ACM Transactions on Computer Systems (TOCS) 32 (1), 1-70, 2014 | 504 | 2014 |
| seL4 enforces integrity T Sewell, S Winwood, P Gammie, T Murray, J Andronick, G Klein International Conference on Interactive Theorem Proving, 325-340, 2011 | 120 | 2011 |
| Don't sweat the small stuff: formal verification of C code without the pain D Greenaway, J Lim, J Andronick, G Klein ACM SIGPLAN Notices 49 (6), 429-439, 2014 | 85 | 2014 |
| Bridging the gap: Automatic verified abstraction of C D Greenaway, J Andronick, G Klein Interactive Theorem Proving: Third International Conference, ITP 2012 …, 2012 | 81 | 2012 |
| 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 | 66 | 2009 |
| Formally verified software in the real world G Klein, J Andronick, M Fernandez, I Kuz, T Murray, G Heiser Communications of the ACM 61 (10), 68-77, 2018 | 58 | 2018 |
| Using Coq to Verify Java CardTM Applet Isolation Properties J Andronick, B Chetali, O Ly Theorem Proving in Higher Order Logics: 16th International Conference …, 2003 | 37 | 2003 |
| A formal approach to constructing secure air vehicle software D Cofer, A Gacek, J Backes, MW Whalen, L Pike, A Foltzer, M Podhradsky, ... Computer 51 (11), 14-23, 2018 | 36 | 2018 |
| Large-scale formal verification in practice: A process perspective J Andronick, R Jeffery, G Klein, R Kolanski, M Staples, H Zhang, L Zhu 2012 34th International Conference on Software Engineering (ICSE), 1002-1011, 2012 | 36 | 2012 |
| Controlled Owicki-Gries concurrency: Reasoning about the preemptible eChronos embedded operating system J Andronick, C Lewis, C Morgan arXiv preprint arXiv:1511.04170, 2015 | 35 | 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 | 31 | 2015 |
| Towards proving security in the presence of large untrusted components J Andronick, D Greenaway, K Elphinstone 5th International Workshop on Systems Software Verification (SSV 10), 2010 | 30 | 2010 |
| Formal verification of security properties of smart card embedded source code J Andronick, B Chetali, C Paulin-Mohring FM 2005: Formal Methods: International Symposium of Formal Methods Europe …, 2005 | 27 | 2005 |
| An empirical research agenda for understanding formal methods productivity R Jeffery, M Staples, J Andronick, G Klein, T Murray Information and software technology 60, 102-112, 2015 | 26 | 2015 |
| 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 | 25 | 2016 |
| seL4 in Australia: from research to real-world trustworthy systems G Heiser, G Klein, J Andronick Communications of the ACM 63 (4), 72-75, 2020 | 24 | 2020 |
| Formally verified system initialisation A Boyton, J Andronick, C Bannister, M Fernandez, X Gao, D Greenaway, ... Formal Methods and Software Engineering: 15th International Conference on …, 2013 | 23 | 2013 |
| An Access Control Model Based Testing Approach for Smart Card Applications: Results of the {POSÉ} Project PA Masson, ML Potet, J Julliand, R Tissot, G Debois, B Legeard, B Chetali, ... JIAS, Journal of Information Assurance and Security 5, 335-351, 2010 | 22 | 2010 |
| Productivity for proof engineering M Staples, R Jeffery, J Andronick, T Murray, G Klein, R Kolanski Proceedings of the 8th ACM/IEEE International Symposium on Empirical …, 2014 | 21 | 2014 |
Gerwin KleinProofcraft and UNSW在 unsw.edu.au 的电子邮件经过验证
