about me

I am a compiler engineer at Runtime Verification, where I work on developing the K Framework, as well as formally verified language implementations in K.

Previously, I completed a PhD at the University of Edinburgh, supervised by Professor Michael O'Boyle. My primary research goal was to improve the integration of heterogenous accelerators and user code, giving compilers new techniques for optimising performance-sensitive workloads. My research focused on two-phase type-directed program synthesis as a way of learning the behaviour of black-box interfaces.

In my free time I play rugby at Lismore RFC.

contact

You can email me at moc.noitacifirevemitnur@eilloc.ecurb, or tweet me at @__inshorts. All my code is on Github.

work and projects

Runtime Verificationaboutrv github
At RV, my work focuses on the development of compiler tooling for the K framework (in particular, the LLVM K backend intended for high-performance concrete execution of programs). Additionally, I have contributed to a standards-compliant K implementation of the C language.
Program SynthesisGithubMSC DissertationPhD Thesis
The main focus of MScR and PhD was the development of program synthesis techniques that aim to learn the behaviour of black-box interfaces. My approach initially used two-phase synthesis driven by type heuristics to synthesise complex control flow, with later work examining additional sources of information to drive synthesis in real-world contexts.
TESLAGithubDissertation
During my MEng I contributed to TESLA, an existing project that allows for temporal assertions to be added to C programs and checked at runtime. I used model-checking to prove that individual assertions could be safely removed, improving the performance of programs using TESLA.
GoCardlessAbout
At GoCardless I was a member of the Core Payments team, responsible for developing the infrastructure used by the company to process Direct Debit transactions. I investigated bugs, contributed to new features, and worked on upgrading legacy code.
PCLGithubDissertation
My undergraduate final project was an implementation of the π-calculus, a minimal expression of concurrent message-passing semantics. I developed a compiler and virtual machine for this language, as well as a library of example programs demonstrating its usage.
RealVNCAbout
At RealVNC I developed a prototype implementation of Apple's CarPlay software to run on the company's internal in-car entertainment platform. This involved writing kernel modules and patches for the Linux kernel's USB subsystem, as well as a driver for the CarPlay protocol.
Other
In 2015 I was responsible for managing the website, ticketing system and admissions for the Trinity Hall June Event, attended by roughly 2000 guests. I have also worked as a freelance iOS and backend developer on a number of projects.