Who I am
I am a research associate working with Matthew Parkinson on the verification of concurrent programs. My research focuses on separation logic and rely-guarantee reasoning.
Previously I was a PhD student working on program safety and graph transformation at the University of York, where I was supervised by Detlef Plump.
My main interests are: proof-based verification; pointer safety; separation logic; graph transformation; concurrent programs.
Update 22/3/09: I have submitted the final version of my PhD thesis. You can read it here.
Publications
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. To appear. (bibtex)
Deny-Guarantee Reasoning (Mike Dodds, Xinyu Feng, Matthew Parkinson, Viktor Vafeiadis). In Proc. 18th European Symposium on Programming (ESOP 2009), LNCS 5502, pages 363-377, Springer-Verlag, 2009. (bibtex) (Technical report with proofs)
From Separation Logic to Hyperedge Replacement and Back (extended abstract) (Mike Dodds). In Proc. International Conference on Graph Transformation (ICGT 2008), LNCS 5214, pages 484-486, Springer-Verlag, 2008. (bibtex)
Graph Transformation in Constant Time (Mike Dodds, Detlef Plump). In Proc. International Conference on Graph Transformation (ICGT 2006), LNCS 4178, pages 367-382. Springer-Verlag, 2006. (bibtex)
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)
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.
Talks and posters
Deny-guarantee reasoning. Talk given at ESOP presenting our paper on deny-guarantee reasoning, March 2009. (The original talk made heavy use of animation, which has made this pdf difficult to understand in parts)
Parametric Shape Analysis via 3-valued Logic. Talk on this paper, given to the Cambridge reading group on verification for C-like languages, February 2009.
Higher-order Interference in Deny-Guarantee. Talk given to London Concurrency Theory Workshop, January 2009.
Deny-guarantee Reasoning (poster). Displayed at Workshop on Linking Tools for Verified Software, December 2008.
Deny-guarantee Reasoning. Talk given at a Computer Lab semantics lunch, November 2008.
Verifying Concurrent Programs. Poster for Computer Lab undergraduate recruitment day, June 2008.
From Separation Logic to Hyperedge Replacement and Back. Talk given at ICGT 2008 doctoral symposium.
Graph Transformation in Constant Time. Talk given at ICGT 2006
Ensuring Pointer Safety through Graph Transformation. Tutorial given at GCM 2006.
Contact Details
| Email: | md466 [@] cl.cam.ac.uk |
| Address: |
William Gates Building 15 JJ Thomson Avenue Cambridge CB3 0FD UK |
| Phone: | +44 (0)1223 763670 |