Mike Dodds

Mike Dodds


Former affiliations

Accepting PhD Students

PhD projects

I am happy to supervise PhD students in any of my areas of interest. These include: multicore data-structures; verification and correctness; program logic; concurrency semantics. 

Personal profile

Research interests

I'm interested in applying the tools of computer science 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.

I am an anniversary lecturer - one of 20 new research-focussed faculty appointed to celebrate the University of York's 50th birthday. My position is roughly equivalent to a tenured assistant professor in the US.



PhD supervisor: Supervisor to Matthew Windsor (York). Second supervisor to Dr. John Wickerson (Cambridge, awarded July 2013). Internal assessor to Samuel Canham and Ivaylo Hristakiev (York).

Academic Service: Reviewer for TOPLAS, POPL, ESOP, ECOOP, APLAS, CONCUR, SAS, and many other top-tier conferences and journals. PC member for CPP 2012, ICE 2014, AVoCS 2014.

Administrative duties: Research Student Training officer. This includes organising training courses, providing triage on training issues, and guiding the annual student-run York Doctoral Symposium. Department seminar organiser. This includes finding speakers, managing the travel budget, and ensuring a broad spectrum of talks.


Employment History

2012- present: Anniversary Research Lecturer, York. Competitively-awarded research lectureship.

2008-2012: Research Associate, Cambridge. EPSRC projects Modular verification of concurrent programs (PI: Matthew Parkinson), jStar: making Java verification practical; (PIs: M. Parkinson & D. Distefano); and Reasoning with Relaxed Memory Models. (PI: P. Sewell).

2004-2008: PhD Computer Science, York. Pointer Safety and Graph Transformation. Supervisor: D. Plump.

2000-2004: MEng CS Software Engineering, York 2000–2004 First-Class Hons.


  • QA75 Electronic computers. Computer science
  • Verification
  • Concurrency
  • Semantics
  • Logic