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, pp. 4 - 4, 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 Katoen JP; Chechik M; Leucker M (eds.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Springer Nature, 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, Association for Computing Machinery (ACM), 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, Institute of Electrical and Electronics Engineers (IEEE), CA, San Jose, pp. 605 - 622, presented at 2015 IEEE Symposium on Security and Privacy, CA, San Jose, 18 May 2015 - 20 May 2015, 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, 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
,