My publications are available from the University of Kent's Academic Repository.
I belong to the following research groups:
I develop rigorous mathematical specifications, testing tools, and verification techniques for real-world concurrent systems, focusing on established interfaces (e.g. C, C++ and, OpenCL) and concrete testable artefacts (e.g. x86, Power, ARM CPUs, and Nvidia, AMD GPUs). My interests span a variety of complementary topics including: empirical testing of the behaviour of hardware and compilers, building formal models of parts of the system, the development of algorithms and data-structures that use fine-grained concurrency, and the verification of those pieces of concurrent code.
If you are interested in discussing the possibility of studying for a PhD related to these topics, please do get in touch. The University of Kent has a variety of internal funding that one can apply for, with deadlines throughout the year.
- Under submission 2017: Compositional Verification of Relaxed-Memory Program Transformations. M. Dodds, M. Batty, A. Gotsman.
- Kent hosted the Kent Concurrency Workshop on the 21st and 22nd of July 2016. This was the next in the series held previously at Imperial, York, Oxford, Dublin, Cambridge, Newcastle, and Queen Mary. Attendance can be judged by inspecting the Doodle poll.
- Kent is hosting the 3rd South of England Regional Programming Language Seminar on the 21st of April 2016, with invited speaker Derek Dreyer talking about Rust, together with many other excellent speakers.
- I recently spoke at a specialist scientific discussion meeting at the Royal Society on verified trustworthy software systems. Find the slides here.
- I have been awarded a Lloyds Register Foundation and Royal Academy of Engineering Research Fellowship, running for 5 years, starting January 2016.
- In December 2015, I was awarded a UK Government Communications Headquarters (GCHQ) Small Grant for travel and equipment.
- The Association of Computing Machinery Special Interest Group on Programming Languages (ACM SIGPLAN) has chosen me as the winner of the John C. Reynolds Doctoral Dissertation Award, 2015.
- The Council of Professors and Heads of Computing (CPHC) and British Computing Society (BCS) have given me their Distinguished Dissertation Award, 2015.
- Overhauling SC atomics in C11 and OpenCL. M. Batty, A. Donaldson, J. Wickerson. In Proc. 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), 2016. peer reviewed, 13 pages.
- Remote-Scope Promotion: Clarified, Rectified, and Verified. J. Wickerson. M. Batty, B. Beckmann, A. Donaldson. In Proc. ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2015. peer reviewed, 17 pages.
- The Problem of Programming Language Concurrency Semantics. M. Batty, K. Memarian, K. Nienhuis, J. Pichon, P. Sewell, In Proc. 24th European Symposium on Programming (ESOP), 2015. peer reviewed, 25 pages.
- GPU concurrency: weak behaviours and programming assumptions. J. Alglave, M. Batty, A. Donaldson, G. Gopalakrishnan, J. Ketema, D. Poetzl, T. Sorensen, J. Wickerson. In Proc. 20th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), 2015. peer reviewed, 15 pages.
- Library Abstraction for C/C++ Concurrency. M. Batty, M. Dodds, A. Gotsman. In Proc. 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), 2013. peer reviewed, 14 pages.
- Synchronising C/C++ and POWER. S. Sarkar, K. Memarian, S. Owens, M. Batty, P. Sewell, L. Maranget, J. Alglave, and D. Williams. In Proc. 33rd ACM SIGPLAN conference on Programming Language Design and Implementation (PLDI), 2012. peer reviewed, 10 pages.
- Clarifying and compiling C/C++ concurrency: from C++0x to POWER. M. Batty, K. Memarian, S. Owens, S. Sarkar, and P. Sewell. In Proc. 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), 2012. peer reviewed, 12 pages.
- Nitpicking C++ concurrency. J. C. Blanchette, T. Weber, M. Batty, S. Owens, and S. Sarkar. In Proc. 13th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP), 2011. peer reviewed, 11 pages.
- Mathematizing C++ concurrency. M. Batty, S. Owens, S. Sarkar, P. Sewell, and T. Weber. In Proc. 38th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL), 2011. peer reviewed, 12 pages.
- Relaxed memory models must be rigorous. F. Z. Nardelli, P. Sewell, J. Ševčík, S. Sarkar, S. Owens, L. Maranget, M. Batty, J. Alglave, In Proc. Exploiting Concurrency Efficiently and Correctly - (EC)2, 2009.
C++ Standard Committee Papers
- N3196: Omnibus Memory Model and Atomics Paper. P. McKenney, M. Batty, C. Nelson, H. Boehm, A. Williams, S. Owens, S. Sarkar, P. Sewell, T. Weber, M.Wong, L. Crowl, B. Kosnik. November 11, 2010.
- N3132: Mathematizing C++ Concurrency: The Post-Rapperswil Model. M. Batty, S. Owens, S. Sarkar, P. Sewell, T. Weber. August 23, 2010.
- N3125: Omnibus Memory Model and Atomics Paper. P. McKenney, M. Batty, C. Nelson, H. Boehm, A. Williams, S. Owens, S. Sarkar, P. Sewell, T. Weber, M.Wong, L. Crowl. August 22, 2010.
- N3136: Coherence Requirements Detailed. M.Wong, B. Kosnik, M. Batty. August 20, 2010.
- N3074: Updates to C++ Memory Model Based on Formalization. P. McKenney, M. Batty, C. Nelson, N.M. Maclaren, H. Boehm, A. Williams, P. Dimov, L. Crowl. March 11, 2010.
- N3045: Updates to C++ Memory Model Based on Formalization. P. McKenney, M. Batty, C. Nelson, N.M. Maclaren, H. Boehm, A. Williams, P. Dimov, L. Crowl. February 15, 2010.
- N3057: Explicit Initializers for Atomics. P. McKenney, M. Batty, C. Nelson, N.M. Maclaren, H. Boehm, A. Williams, P. Dimov, L. Crowl. March 11, 2009.
- N2955: Comments on the C++ Memory Model Following a Partial Formalization Attempt. M. Batty. September 28, 2009.