My research is about using rigorous mathematics to solve tricky engineering problems. At the moment, I'm mostly interested building and verifying multicore data-structures.
I am an anniversary lecturer - one of 20 new faculty appointed to celebrate the University of York's 50th birthday. My position is roughly equivalent to a tenured assistant professor in the US.
I tweet about CS and personal things as @miike.
I'm interested in applying the tools of CS theory - logic, proof, and formal semantics - to tricky engineering problems.
Most of my work is about verification - essentially, using maths to guarantee that software can't go wrong. My main targets are the concurrent data-structures that lie at the heart of multicore systems. These are key systems components, but they're also particularly hard to get right.
I've often worked on program logic, in particular Concurrent Abstract Predicates, which I co-developed. More recently, I've worked on correctness conditions and data-structure design. I've also dabbled in automated reasoning and graphical proof visualisation.
My complete list of papers are available on my publication list.