Select Publications
Journal articles
1997, 'Modeling and Simulation of Tunneling through Ultra-Thin Gate Dielectrics', Journal of Applied Physics, pp. 7900 - 7908
,1996, 'Improved modelling of grain boundary recombination in bulk and p-n junction regions of polycrystalline silicon solar cells', Journal of Applied Physics, pp. 6783 - 6795
,1996, 'Numerical quantification and minimisation of perimeter losses in high-efficiency silicon solar cells', Progress in Photovoltaics, pp. 355 - 367
,1996, 'Rear serface passivation of high-efficiency silicon solar cells by a floating junction', Journal of Applied Physics, pp. 3574 - 3586
,1996, 'Spatially resolved analysis and minimisation of resistive losses in high-efficiency Si solar cells', Progress in Photovoltaics, pp. 399 - 414
,1995, 'Limiting loss mechanisms in 23% efficient silicon solar cells', Journal of Applied Physics, pp. 3491 - 3501
,1995, 'Recombination rate saturation mechanisms at oxidized surfaces of high-efficiency silicon solar cells', Journal of Applied Physics, pp. 4740 - 4754
,1995, 'Two-dimensional numerical simulations of high-efficiency silicon solar cells', Microelectronics Journal, pp. 273 - 286
,1994, 'Innovative structures for thin film crystalline silicon solar cells to give high efficiencies from low quality silicon', Conference Record of the IEEE Photovoltaic Specialists Conference, 2, pp. 1563 - 1566
,1994, 'Two-dimensional numerical optimization study of the rear contact geometry of high-efficiency silicon solar cells', Journal of Applied Physics, 75, pp. 5391 - 5405, http://dx.doi.org/10.1063/1.355694
,1994, 'Two-dimensional minority carrier flow in high-efficiency silicon solar cells at short-circuit, open-circuit and maximum power point operating conditions', Solar Energy Materials and Solar Cells, 34, pp. 149 - 160, http://dx.doi.org/10.1016/0927-0248(94)90035-3
,1994, 'Decreased emitter sheet resistivity loss in high‐eficiency silicon solar cells', Progress in Photovoltaics: Research and Applications, 2, pp. 3 - 17, http://dx.doi.org/10.1002/pip.4670020103
,1991, 'Three-Dimensional Numerical Semiconductor Device Simulation: Algorithms, Architectures, Results', IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 10, pp. 1218 - 1230, http://dx.doi.org/10.1109/43.88918
,1986, 'A Portable Operating System Interface and Utility Library', IEEE Software, 3, pp. 18 - 26, http://dx.doi.org/10.1109/MS.1986.229470
,Conference Papers
2023, 'AutoCC: Automatic Discovery of Covert Channels in Time-Shared Hardware', in Proceedings of the 56th Annual IEEE/ACM International Symposium on Microarchitecture, MICRO 2023, pp. 871 - 885, http://dx.doi.org/10.1145/3613424.3614254
,2023, 'Pancake: Verified Systems Programming Made Sweeter', in PLOS 2023 - Proceedings of the 12th Workshop on Programming Languages and Operating Systems, Part of: SOSP 2023, pp. 1 - 9, http://dx.doi.org/10.1145/3623759.3624544
,2023, 'First steps in verifying the seL4 Core Platform', in APSys 2023 - Proceedings of the 14th ACM SIGOPS Asia-Pacific Workshop on Systems, pp. 9 - 15, http://dx.doi.org/10.1145/3609510.3609821
,2023, 'Tutorial: Using the seL4 Microkernel', in 2023 53rd Annual IEEE/IFIP International Conference on Dependable Systems and Networks - Supplemental Volume (DSN-S), IEEE, presented at 2023 53rd Annual IEEE/IFIP International Conference on Dependable Systems and Networks - Supplemental Volume (DSN-S), 27 June 2023 - 30 June 2023, http://dx.doi.org/10.1109/dsn-s58398.2023.00016
,2023, 'Formalising the Prevention of Microarchitectural Timing Channels by Operating Systems', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Lübeck, Germany, pp. 103 - 121, presented at Formal Methods (FM 2023), Lübeck, Germany, 06 March 2023 - 10 March 2023, http://dx.doi.org/10.1007/978-3-031-27481-7_8
,2023, 'Verified Value Chains, Innovation and Competition', in Proceedings of the 2023 IEEE International Conference on Cyber Security and Resilience, CSR 2023, pp. 470 - 476, http://dx.doi.org/10.1109/CSR57506.2023.10224911
,2023, 'Pancake: Verified Systems Programming Made Sweeter.', in PLOS@SOSP, ACM, pp. 1 - 9, https://doi.org/10.1145/3623759
,2022, 'Property-Based Testing: Climbing the Stairway to Verification', in SLE 2022 - Proceedings of the 15th ACM SIGPLAN International Conference on Software Language Engineering, co-located with SPLASH 2022, pp. 84 - 97, http://dx.doi.org/10.1145/3567512.3567520
,2022, 'Can We Put the 'S' Into IoT?', in 2022 IEEE 8th World Forum on Internet of Things, WF-IoT 2022, http://dx.doi.org/10.1109/WF-IoT54382.2022.10152198
,2021, 'Microarchitectural Timing Channels and their Prevention on an Open-Source 64-bit RISC-V Core', in Proceedings -Design, Automation and Test in Europe, DATE, pp. 627 - 632, http://dx.doi.org/10.23919/DATE51398.2021.9474214
,2019, 'Fault Tolerance Through Redundant Execution on COTS Multicores: Exploring Trade-Offs', in Proceedings - 49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks, DSN 2019, pp. 188 - 200, http://dx.doi.org/10.1109/DSN.2019.00031
,2019, 'SoK: Benchmarking flaws in systems security', in Proceedings - 4th IEEE European Symposium on Security and Privacy, EURO S and P 2019, pp. 310 - 325, http://dx.doi.org/10.1109/EuroSP.2019.00031
,2019, 'Can We Prove Time Protection?', in Proceedings of the Workshop on Hot Topics in Operating Systems, HotOS 2019, pp. 23 - 29, http://dx.doi.org/10.1145/3317550.3321431
,2019, 'Time protection: The missing OS abstraction', in Proceedings of the 14th EuroSys Conference 2019, http://dx.doi.org/10.1145/3302424.3303976
,2019, 'Message from the 2012 USENIX annual technical conference program co-chairs', in Proceedings of the 2012 USENIX Annual Technical Conference, USENIX ATC 2012, pp. VII
,2019, 'VNUMA: A virtual shared-memory multiprocessor', in Proceedings of the 2009 USENIX Annual Technical Conference, pp. 15 - 28
,2018, 'No security without time protection: We need a new hardware-software contract', in Proceedings of the 9th Asia-Pacific Workshop on Systems, APSys 2018, http://dx.doi.org/10.1145/3265723.3265724
,2018, 'The Jury is in: Monolithic OS design is flawed: Microkernel-based designs improve security', in Proceedings of the 9th Asia-Pacific Workshop on Systems, APSys 2018, http://dx.doi.org/10.1145/3265723.3265733
,2018, 'Scheduling-Context Capabilities: A Principled, Light-Weight Operating-System Mechanism for Managing Time', in EuroSys '18: Thirteenth EuroSys Conference 2018, April 23--26, 2018, Porto, Portugal, Portugal, presented at Thirteenth EuroSys Conference 2018, Portugal, 23 April 2018 - 26 March 2018, http://dx.doi.org/10.1145/3190508.3190539
,2017, 'The COGENT case for property-based testing', in Proceedings of the 9th Workshop on Programming Languages and Operating Systems, PLOS 2017, Shanghai, China, pp. 1 - 7, presented at 9th Workshop on Programming Languages and Operating Systems, Shanghai, China, 28 October 2017 - 28 October 2017, http://dx.doi.org/10.1145/3144555.3144556
,2017, 'A performance evaluation of rump kernels as a multi-server OS building block on seL4', in Proceedings of the 8th Asia-Pacific Workshop on Systems, APSys 2017, Mumbai, India, presented at APSys '17 Proceedings of the 8th Asia-Pacific Workshop on Systems, Mumbai, India, 02 September 2017 - 02 September 2017, http://dx.doi.org/10.1145/3124680.3124727
,2016, 'Complete, High-Assurance Determination of Loop Bounds and Infeasible Paths for WCET Analysis', in 2016 IEEE Real-Time and Embedded Technology and Applications Symposium, RTAS 2016 - Proceedings, Vienna, AUSTRIA, presented at 22nd IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS), Vienna, AUSTRIA, 11 April 2016 - 14 April 2016, http://dx.doi.org/10.1109/RTAS.2016.7461326
,2016, 'COGENT: Verifying high-assurance file system implementations', in International Conference on Architectural Support for Programming Languages and Operating Systems - ASPLOS, Atlanta, GA, USA, pp. 175 - 188, presented at 21st International Conference on Architectural Support for Programming Languages and Operating Systems, Atlanta, GA, USA, 02 April 2016 - 06 April 2016, http://dx.doi.org/10.1145/2872362.2872404
,2016, 'CATalyst: Defeating last-level cache side channel attacks in cloud computing', in Proceedings - International Symposium on High-Performance Computer Architecture, Barcelona, SPAIN, pp. 406 - 418, presented at 22nd IEEE International Symposium on High-Performance Computer Architecture (HPCA), Barcelona, SPAIN, 12 March 2016 - 16 March 2016, http://dx.doi.org/10.1109/HPCA.2016.7446082
,2015, 'For a Microkernel, a Big Lock Is Fine', in APSys '15 Proceedings of the 6th Asia-Pacific Workshop on Systems, ACM, Tokyo, Japan, presented at ACM Asia-Pacific Workshop on Systems (APSys), Tokyo, Japan, 27 July 2015 - 28 July 2015, http://dx.doi.org/10.1145/2797022.2797042
,2015, 'Report on the Asia-Pacific Systems Workshop 2015 (APSys'15)', in OPERATING SYSTEMS REVIEW, ASSOC COMPUTING MACHINERY, JAPAN, Tokyo, pp. 1 - 2, presented at 6th Asia-Pacific Systems Workshop (APSys), JAPAN, Tokyo, 27 July 2015 - 28 July 2015, http://dx.doi.org/10.1145/2903267.2903269
,2015, 'Last-level cache side-channel attacks are practical', in Proceedings - IEEE Symposium on Security and Privacy, pp. 605 - 622, http://dx.doi.org/10.1109/SP.2015.43
,2014, 'Mixed-Criticality Support in a High-Assurance, General-Purpose Microkernel', in Davis R; Cucu-Grosjean L (ed.), 2nd International Workshop on Mixed Criticality Systems, 2nd Workshop on Mixed Criticality Systems, Rome, Italy, pp. 9 - 14, presented at 2nd Workshop on Mixed Criticality Systems, Rome, Italy, 01 December 2014 - 01 December 2014, http://www.nicta.com.au/pub?doc=8354
,2014, 'The last mile: An empirical study of timing channels on seL4', in Proceedings of the ACM Conference on Computer and Communications Security, pp. 570 - 581, http://dx.doi.org/10.1145/2660267.2660294
,2014, 'File systems deserve verification too!', in Operating Systems Review (ACM), pp. 58 - 64, http://dx.doi.org/10.1145/2626401.2626414
,2014, 'Mobile multicores: Use them or waste them', in Operating Systems Review (ACM), pp. 44 - 48, http://dx.doi.org/10.1145/2626401.2626411
,2014, 'Trickle: Automated infeasible path detection using all minimal unsatisfiable subsets', in Real-Time and Embedded Technology and Applications Symposium - Proceedings, Berlin, presented at Real-Time and Embedded Technology and Applications Symposium, Berlin, 15 April 2014 - 17 April 2014
,2014, 'Unifying DVFS and offlining in mobile multicores', in Real-Time and Embedded Technology and Applications - Proceedings, Berlin, presented at Real-Time and Embedded Technology and Applications, Berlin, 15 April 2014 - 17 April 2014
,2013, 'From L3 to seL4: What have we learnt in 20 years of L4 microkernels?', in SOSP 2013 - Proceedings of the 24th ACM Symposium on Operating Systems Principles, pp. 133 - 150, http://dx.doi.org/10.1145/2517349.2522720
,2013, 'Mobile Multicores: Use Them or Waste Them', in Proceedings of the 5th Workshop on Power-Aware Computing and Systems, ACM, Farmington, PA, USA, presented at 5th Workshop on Power-Aware Computing and Systems, Farmington, PA, USA, 03 November 2013 - 03 November 2013
,2013, 'A scalable lock manager for multicores', in Proceedings of the ACM SIGMOD International Conference on Management of Data, pp. 73 - 84, http://dx.doi.org/10.1145/2463676.2465271
,