June Andronick
June Andronick
Principal Research Scientist, Data61, CSIRO
Verified email at - Homepage
Cited by
Cited by
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
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
seL4 enforces integrity
T Sewell, S Winwood, P Gammie, T Murray, J Andronick, G Klein
International Conference on Interactive Theorem Proving, 325-340, 2011
Bridging the gap: Automatic verified abstraction of C
D Greenaway, J Andronick, G Klein
International Conference on Interactive Theorem Proving, 99-115, 2012
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
Mind the gap
S Winwood, G Klein, T Sewell, J Andronick, D Cock, M Norrish
International Conference on Theorem Proving in Higher Order Logics, 500-515, 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
Using Coq to Verify Java CardTM Applet Isolation Properties
J Andronick, B Chetali, O Ly
International conference on theorem proving in higher order logics, 335-351, 2003
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
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
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
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
Formal verification of security properties of smart card embedded source code
J Andronick, B Chetali, C Paulin-Mohring
International Symposium on Formal Methods, 302-317, 2005
Controlled Owicki-Gries concurrency: Reasoning about the preemptible eChronos embedded operating system
J Andronick, C Lewis, C Morgan
arXiv preprint arXiv:1511.04170, 2015
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
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
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
Formally verified system initialisation
A Boyton, J Andronick, C Bannister, M Fernandez, X Gao, D Greenaway, ...
International Conference on Formal Engineering Methods, 70-85, 2013
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
The road to trustworthy systems
G Heiser, J Andronick, K Elphinstone, G Klein, I Kuz, L Ryzhyk
Proceedings of the fifth ACM workshop on Scalable trusted computing, 3-10, 2010
The system can't perform the operation now. Try again later.
Articles 1–20