Honours Class 1 and The University Medal
Thesis: Evaluating Programming Languages for Verified OS Components
Supervised by Scientia Professor Gernot Heiser
Designed and implemented an anti-rollback mechanism for EOS SWI in Aboot, preventing downgrades to potentially vulnerable firmware versions
Integrated with secure boot and measured boot chain of trust, leveraging TPM for persistent rollback protection state
Resolved bugs and performed code refactors across the EOS codebase in C/C++
Conducted classes for COMP6771 Advanced C++ Programming and COMP9242 Advanced Operating Systems
Guided students through systems programming concepts, modern C++ features, and OS-level design principles
Provided feedback on assignments and assisted students during consultation hours
Contributed to LionsOS, a component-based operating system built on the seL4 verified microkernel, designed for building custom, task-specific systems from composable components
Implemented core migration and offlining mechanisms for multicore management in LionsOS
Built a userspace webserver as a LionsOS component using its lock-free queue-based communication model
Created a proof-of-concept transpiler to convert C code into Pancake, a research language with verified compilation for writing formally verified OS components
Developed BAMBINO-LM, a continual pre-training approach for small-scale language models inspired by bilingual language acquisition in children
Combined language alternation strategies with PPO-based perplexity rewards to enable cross-lingual transfer between English and Italian
Published at the Workshop on Cognitive Modeling and Computational Linguistics (CMCL) 2024