- RV-CuBES I am co-organising a Workshop focused on Competitions, Benchmarks, Evaluation and Standardisation of RV tools colocated with RV 2017.
- SMT-COMP'17 I am helping co-organise this year's iteration of SMT-COMP. The Call for Comments has been published; please read.
- Dagstuhl Seminar Our Dagstuhl Seminar on Behavioural Specification (Languages for RV) has been accepted and will run in November.
- SYNASC 2017 I am on the PC for the Logic and Programming track of the 19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing. Please consider submitting.
- PrePost 2017 I am on the PC for the 2nd International Workshop on Pre- and Post-Deployment Verification Techniques. Please consider submitting.
- RV CFP The CFP for RV 2017 has been published. Please consider submitting.
- IWIL 2017 I am on the PC for the 12th International Workshop on the Implementation of Logics. Please consider submitting.
- ARCADE 2017 I am co-organising The First ARCADE Workshop on the future of automated reasoning, to be held in association with CADE-26 in August
- RV 2017 I am co-PC chair for The 17th International Conference on Runtime Verification which will be held in Seattle 13-16 September
- ISoLA 2016 (Oct 16) I presented two RV papers at the 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation in Corfu.
- GCAI 2016 (Oct 16) Martin presented two of our papers on theory reasoning and clausification at the 2nd Global Conference on Artificial Intelligence in Berlin.
- RV 2016 (Sep 16) An overview of MarQ was presented at The 16th International Conference on Runtime Verificaiton in Madrid.
- RV Summer School (Sep 16) I taught on the 1st ARVI COST Summer School on Runtime Verification" talking about Performance Issues and Optimisation (at RV16).
- RV Competition The results of the Third International Competition on Runtime Verification" are available, well done everybody.
- SAT 2016 (July 16) Martin presented our recent work on finite model finding at the 19th International Conference on Theory and Applications of Satisfiability Testing in Bordeaux.
- SMTCOMP 2016 Vampire won three tracks in the 11th International Satisfiability Modulo Theories Competition. This is the first time we entered.
- CASC-J8 Vampire won 4 divisions at CASC-J8, the world-cup of theorem provers.
- IJCAR 2016 (July 16) I presented a paper on literal selection at the International Joint Conference on Automated Reasoning 2016 in Coimbra.
- Vampire 2016 (July 16) I presented two papers at the The Third Vampire Workshop at IJCAR.
- News...! (July 16) I have started this news section, for previous activities see publications etc.
I am a Lecturer in the School of Computer Science at the University of Manchester. I belong to the Formal Methods Group .
I have two main areas of interest. The first is Theorem Proving. I am one of the developers of the Vampire first-order ATP system, joining the team in 2014. I am interested in theoretical and practical extensions that improve the prover's performance, applicability and usability. The second area of interest is Runtime Verification. I develop the MarQ monitoring tool, help organise the RV competition, and am a working group leader on a RV Cost Action. See the relevant pages on this site for more information.
I am keen to collaborate on new research projects and to supervise able and interested PhD students. Please see my Research page for an idea of what I do and feel free to contact me with any thoughts.
I was previously a Postdoctoral Research Associate (2014-2016) and PhD Student (2010-2014) in the same research group. My postdoc started my work on the Vampire system where I looked at finite model finding, theory reasoning and collaborative provers. My PhD was on runtime verification, looking at specification languages and monitoring algorithms, and specification mining.