Compositional Verification of Relaxed-Memory Program Transformations (Mike Dodds, Mark Batty, Alexey Gotsman). [Stellite tool.] Under review.
Verifying Custom Synchronisation Constructs Using Higher-Order Separation Logic (Mike Dodds, Suresh Jagannathan, Matthew J Parkinson, Kasper Svendsen, Lars Birkedal). Transactions on Programming Languages and Systems (TOPLAS) 38(2): 4. 2016.
Proof-directed Parallelization Synthesis by Separation Logic (Matko Botincan, Mike Dodds and Suresh Jagannathan). Transactions on Programming Languages and Systems (TOPLAS) 35(2): 8. 2013.
Starling: Lightweight Concurrency Verification With Views (Matthew Windsor, Mike Dodds, Ben Simner, Matthew J Parkinson). [Starling tool.] Computer Aided Verification (CAV 2017).
Proving Linearizability Using Partial Orders (Artem Khyzha, Mike Dodds, Alexey Gotsman, Matthew Parkinson). European Symposium on Programming (ESOP 2017).
Learning Assertions to Verify Linked-List Programs (Jan Tobias Muehlberg, David H. White, Mike Dodds, Gerald Luettgen, Frank Piessens). In Software Engineering and Formal Methods (SEFM 2015)
A Scalable, Correct Time-stamped Stack (Mike Dodds, Andreas Haas, Christoph Kirsch ). In Principles of Programming Languages (POPL 2015)
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]
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]
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]
Starling: Stress-Free Concurrency Verification (Matt Windsor, Mike Dodds, Ben Simner, and Matthew J. Parkinson). 2016 York Doctoral Symposium.
Towards Rigorously Faking Bidirectional Model Transformations (Christopher M Poskitt, Mike Dodds, Richard F Paige, Arend Rensink). In Third Workshop on the Analysis of Model Transformations (AMT 2014).
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]
Evidence for the Flipped Classroom in STEM (Mike Dodds). Survey paper written for York's PGCAP teaching qualification.
Abstraction Refinement for Separation Logic Program Analyses (Matko Botincan, Mike Dodds and Stephen Magill). Unpublished.
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]