bruce collie

about me

Previously, I was the lead developer of the K Framework at Runtime Verification. K is a framework for developing mechanised operational semantics of programming languages. I was responsible for developing the underlying compiler technology, specifying and developing commercial language implementations using K, and managing the development of the broader K tooling ecosystem.

I hold a PhD from the University of Edinburgh, supervised by Professor Michael O'Boyle. My research focused on two-phase, type-directed program synthesis as a way of learning the behaviour of black-box interfaces, at the intersection of formal methods and systems research.

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, and you can get an up-to-date copy of my CV here.

resume

education

  • University of Edinburgh (2018–2021)
    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

research

  • 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

employment

  • Monad Labs(2024–)about
  • Runtime Verification(2021–24)aboutrv github
    At RV, I was the lead developer for the K Framework tooling ecosystem. As well as working on the development of internal compiler tooling for K (in particular, the LLVM K backend intended for high-performance concrete execution of programs), I had broad leadership responsibilities for the company's usage of K across a number of commercial projects and engagements.
  • PhD Research(2017–2021)GithubMSC DissertationPhD Thesis
    The main focus of my 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.
  • GoCardless(2016)About
    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.
  • RealVNC(2015)About
    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.