I am a research lecturer working on concurrency theory, program logics, and algorithm verification.

Activities

I'm organising the York Concurrency Workshop 2014.

Papers

A Scalable, Correct Time-stamped Stack (Mike Dodds, Andreas Haas, Christoph Kirsch ). In Principles of Programming Languages (POPL 2015)

Abstraction Refinement for Separation Logic Program Analyses (Matko Botincan, Mike Dodds and Stephen Magill). (Draft)

Proof-directed Parallelization Synthesis by Separation Logic (Matko Botincan, Mike Dodds and Suresh Jagannathan). Journal paper, accepted for Transactions on Programming Languages and Systems (TOPLAS) 35(2): 8.

C/C++ Causal Cycles Confound Compositionality (Mike Dodds, Mark Batty and Alexey Gotsman). Tiny Transactions on Computer Science, Volume 2.

Ribbon Proofs for Separation Logic (John Wickerson, Mike Dodds, and Matthew J. Parkinson). In European Symposium on Programming (ESOP 2013) [bibtex] [Extended abstract] [Isabelle proofs]

Library Abstraction for C/C++ Concurrency (Mark Batty, Mike Dodds and Alexey Gotsman). In Principles of Programming Languages (POPL 2013) [bibtex]

Resource-Sensitive Synchronization Inference by Abduction (Matko Botincan, Mike Dodds, and Suresh Jagannathan). In Principles of Programming Languages (POPL 2012) [bibtex] [Technical report with proofs]

Safe Asynchronous Multicore Memory Operations (Matko Botincan, Mike Dodds, Alastair F. Donaldson, and Matthew J. Parkinson). In Automated Software Engineering (ASE 2011). [bibtex]

A Simple Abstraction for Complex Concurrent Indexes (Pedro da Rocha Pinto, Thomas Dinsdale-Young, Mike Dodds, Philippa Gardner, Mark Wheelhouse). In Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 2011). [bibtex] [Technical report with proofs]

jStar-eclipse: an IDE for Automated Verification of Java Programs (Daiva Naudziuniene, Matko Botincan, Dino Distefano, Mike Dodds, Radu Grigore and Matthew J. Parkinson). In European Software Engineering Conference / Foundations of Software Engineering (ESEC/FSE'2011). [bibtex]

Modular Reasoning for Deterministic Parallelism (Mike Dodds, Suresh Jagannathan and Matthew J. Parkinson). In Principles of Programming Languages (POPL 2011). [bibtex]

Concurrent Abstract Predicates (Thomas Dinsdale-Young, Mike Dodds, Philippa Gardner, Matthew J. Parkinson and Viktor Vafeiadis). In Proc. 24th European Conference on Object-Oriented Programming (ECOOP 2010). [bibtex] [Technical report with proofs]

Explicit Stabilisation for Modular Rely-Guarantee Reasoning (John Wickerson, Mike Dodds and Matthew J. Parkinson). In Proc. 19th European Symposium on Programming (ESOP 2010). [bibtex] [Technical report with proofs]

Deny-Guarantee Reasoning (Mike Dodds, Xinyu Feng, Matthew J. Parkinson and Viktor Vafeiadis). In Proc. 18th European Symposium on Programming (ESOP 2009), LNCS 5502, pages 363-377, Springer-Verlag, 2009. [bibtex] [Technical report with proofs]

Graph Transformation in Constant Time (Mike Dodds, and Detlef Plump). In Proc. International Conference on Graph Transformation (ICGT 2006), LNCS 4178, pages 367-382. Springer-Verlag, 2006. [bibtex]

Workshop Papers

coreStar: The Core of jStar (Matko Botincan, Dino Distefano, Mike Dodds, Radu Grigore, Daiva Naudziuniene, Matthew J. Parkinson). In Boogie 2011: First International Workshop on Intermediate Verification Languages. [bibtex]

From Separation Logic to Hyperedge Replacement and Back (Mike Dodds, Detlef Plump). In Proc. Doctoral Symposium at the International Conference on Graph Transformation, Electronic Communications of the EASST, 2009. [bibtex] [Short version]

Extending C for Checking Shape Safety (Mike Dodds, Detlef Plump). In Proc. Graph Transformation for Verification and Concurrency (GT-VC 2005), ENTCS 154(2). Elsevier, 2006. [bibtex]

Other Publications

Automatic Safety Proofs for Asynchronous Memory Operations [poster] (Matko Botincan, Mike Dodds, Alastair Donaldson and Matthew J. Parkinson). In Principles and Practice of Parallel Programming (PPoPP 2011). [bibtex]

Graph Transformation and Pointer Structures (Mike Dodds, PhD Thesis), Viva date: January '09. Graduation: August '09.

Using Trace Data to Diagnose Non-Termination Errors (Mike Dodds, Colin Runciman). In Proc. Hat Day 2005: work in progress on the Hat tracing system for Haskell, pages 12-17. Tech. Report YCS-2005-395, Dept. of Computer Science, University of York, UK, 2005. [bibtex]

What I do

Software, unlike most other engineered artifacts, rarely does exactly what we want. The designers of bridges or car engines can generally ensure that their designs will work as intended. In contrast, even well-tested software often behaves in unexpected ways, often by crashing or corrupting information. The consequences of defective software can be severe, including millions of pounds of economic damage and substantial numbers of deaths.

The aim of program verification is to ensure that software behaves as we expect. Programs cannot simply be tested to ensure correct behaviour; there are simply too many possible inputs. Instead we must reason formally about programs to show that they conform to specification.

Programming languages such as Java and C store complex data as so-called pointer structures. Programs that use pointer structures are, however, amongst the most difficult to verify, because pointers permit aliasing, which means that local operations can have global effects. While some progress has been made in verifying other programs, verifying pointer manipulating programs is one of the major outstanding challenges in computer science.

In my research I work on using abstraction to verify so-called concurrent pointer programs, that is, pointer programs that interact with other programs. Concurrent programs have traditionally been viewed as difficult to reason about, but concurrency is now built into the hardware of almost all new computers, making it unavoidable. By modelling concurrent programs abstractly, some of the complexity can be hidden, making verification possible.

Contact Details

Email: mike.dodds [@] york.ac.uk
Address: Department of Computer Science
University of York
Deramore Lane
York YO10 5GH, UK
Phone: +44 (0)1904 325444