bruce collie

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.


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



  • Program Lifting using Gray-Box Behavior
    Conference Paper at PACT 2021pdf
  • Modeling Black-Box Components with Probabilistic Synthesis
    Conference Paper at GPCE 2020ACMpdf
    best paper
  • M3: Semantic API Migration
    Conference Paper at ASE 2020IEEEpdf
  • Retrofitting Symbolic Holes to LLVM IR
    Workshop Presentation at TyDe 2020pdfvideo
  • Automatically Harnessing Sparse Acceleration
    Conference Paper at CC 2020ACMpdf
  • Type-Directed Program Synthesis and Constraint Generation for Library Portability
    Conference Paper at PACT 2019IEEEpdfslides
  • Augmenting Type Signatures for Program Synthesis
    Workshop Presentation at TyDe 2019pdfslides


  • University of Edinburgh (2018–2022)
    PhD Pervasive Parallelism
  • University of Edinburgh (2017–18)
    MScR Pervasive Parallelism: Distinction
  • University of Cambridge (2016–17)
    MEng Computer Science: Distinction
  • University of Cambridge (2013–16)
    BA Computer Science: 1st Class

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.
  • 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.
  • 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.
  • 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.