News
- Competition Success(Summer 2020) Vampire has won awards at SMTCOMP and CASC. In SMTCOMP we came 2nd/3rd for a few categories in the largest contribution/biggest lead awards and we won one or more medals in 11 divisions (logics). In CASC we placed first in arithmetic, theorems, and non-theorems, and made a big jump forward in higher-order.
- SCorCH Announced.(June 2020) I am excited to announce the new Secure Code for Capability Hardware (SCorCH) project. This is a 42 month project with over £1.3M of funding from ISCF/EPSRC in collaboration with the University of Oxford, ARM, and AWS. See the website for adverts for open positions.
- PAAR Papers/Talks. My PhD student Michael Rawson presented our work on machine learning and automated theorem proving at The 7th Workshop on Practical Aspects of Automated Reasoning
- IJCAR Papers. I have three joint papers with my PhD student Ahmed Bhayat at the International Joint Conference on Automated Reasoning. These papers explore higher-order reasoning in Vampire and represent an exciting step forward in automated higher-order theorem proving.
- PostDoc Position.(January 2020) We're advertising for a postdoctoral research associate position to work on theory reasoning in Vampire.
- SMTCOMP Journal Paper. I have coauthored a paper summarising and analysing the last three years of SMTCOMP has been published in JSAT.
- CADE and FroCoS Presentations We have presented three papers at the 27th International Conference on Automated Deduction and two papers at the 12th International Symposium on Frontiers of Combining Systems. These papers describe recent efforts in automating inductive reasoning, higher-order reasoning, and applying machine learning to automated theorem proving.
- CASC Success.(August 2019) Vampire has picked up five trophies at CASC this year (FOF, TFA, FNT, EPR, FEW). Well done to everybody who contributed.
- SMT-COMP Success. Vampire has enjoyed another year of success at SMT-COMP. See here and here.
- Invited Talk. I have just presetend an invited talk at VORTEX 2019 : 3rd International Workshop on Verification of Objects at Runtime Execution
- Paper accepted at RV. Joshua Dawes and I have had a paper on violation explanation for CFTL accepted to the 19th International Conference on Runtime Verification.
- Two papers accepted at FroCoS. We have two papers accepted at the 12th International Symposium on Frontiers of Combining Systems.
- The first paper is with student Michael Rawson and presents a neurally guided theorem prover for first-order logic.
- The second is with Martin Riener and Martin Suda and explores symmetry avoidance for MACE-Style finite model building.
- Three papers accepted at CADE. My group has had three papers accepted at the 27th International Conference on Automated Deduction.
- The first paper, co-authored with student Ahmed Bhayat introduces a form of combinatory unification for higher-order reasoning in Vampire.
- The second paper, co-authored with student Michael Rawson explores a dynamic form of clause selection (in Vampire).
- The third paper, co-authored with Andrei Voronkov looks at incorproating induction into Vampire.
- Paper Success. My student Joshua Dawes has had two papers accepted on his work on Runtime Verification. The first, to be presented at SAC presents a new specification language and the second, to be presented at TACAS presents his VyPR tool for monitoring Python programs.
- Submit your Papers! I will be serving on the PCs of FMCAD, TABLEAUX, and RV. Please consider submitting your papers here!
- SMT-COMP 19. I am co-chairing the 2019 SMT competition
- RVBC 18. I announced the results of the 2018 RV Benchmark Challenge at RV 2018. Keep an eye on the competition website for details of future competitions.
- RV 2018. I attend RV 2018 in November and presented two papers. The first is a taxonomy for RV and the second an approach for translating parametric trace slicing based specifications to rule systems. See my publications page for details.
- CADE 2019. I am workshop chair for CADE-27. Please submit workshop proposals and papers. And attend the exciting workshops and conference in Natal, Brazil!
- Competition Success! Vampire has won three trophies at CASC (results here) for first-order theorems, first-order non-theorems, and typed first-order with arithmetic. It has also won three divisions in SMT-COMP (results here). We got given three medals at the FLoC Olympic Games
- FLoC I have attended the Federated Logic Conference 2018 and presented work at the 5th Vampire workshop, 16th SMT Workshop, 3rd ARQNL Workshop, and 6th PAAR Workshop. See publications for slides and papers.
- TACAS paper Martin Suda presented our TACAS paper on unification with abstraction and theory instantiation (see publications page).
- Lectureship Advertised Manchester are advertising for a Lecturer in Program Analysis and Cyber Security (Open to the application of Formal Methods to Cyber Security in general).
- RV Book. I have co-authored two chapters in a new Open Access Runtime Verification Book. See my chapters on my publications page.
- PAAR 2018 I am on the PC for the 6th Workshop on practical aspects of automated reasoning. Please consider submitting.
- ARQNL 2018 I am an invited speaker for the 3rd International Workshop on Automated Reasoning in Quantified Non-Classical Logics where I will present recent work in Vampire.
- RV 2018 I am on the PC for the 18th International Conference on Runtime Verification. Please consider submitting.
- FMCAD 2018 I am on the PC for the 18th International Conference on Formal Methods in Computer-Aided Design. Please consider submitting.
- ATVA 2018 I am on the PC for the 16th International Symposium on Automated Technology for Verification and Analysis. Please consider submitting.
- ISoLA 2018 I am co-organising a track A Broader View on Verification: From Static to Runtime and Back at the 8th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation.
- QuTie We have begun a new EPSRC-funded project exploring theory reasoning in Vampire. The first step has been to hire Martin Riener to join the Vampire team.
- Vampire Update Vampire has a new website and the source code is now available on GitHub.
- ARCADE Proceedings The ARCADE proceedings have been published
- ASE 17 Tutorial (Oct 17) All the material from our tutorial on Vampire can be found here.
- Preprint We have a new preprint on our work on theory reasoning in Vampire.
- PrePost I have given a talk (via Skype for the first time) at the 2nd PrePost Workshop on using static detection of garbage events to improve runtime monitoring.
- RV Proceedings The RV 2017 proceedings have been published by Springer.
- Vampire Tutorial at ASE I will be attending ASE 2017 (Urbana-Champaign, Illinois) to present a tutorial on Vampire and its applications to rigorous systems engineering. Please join me, it will be fun!
- Positions We have a PostDoc position available in the Vampire group and the school has two positions (Lecturer and Prof) available in the area of program analysis with applications in cyber security.
- KimFest Klaus presented our paper about Runtime Verification Logics at KIMFest, a conference in honour of Kim Larsen in Aalborg.
- CASC-26 Vampire won five divisions in this year's competition, defending our titles won last year.
- Vampire Workshop 2017 I have given two talks at the Vampire workshop in Gothenburg about Incremental Solving with Vampire and Revisiting Question Answering in Vampire
- ARCADE 2017 took place in Gothenburg on the 6th August and led to some lively discussion (see slides). Watch this space for a fuller report
- SMTCOMP 2017 Vampire won 4 tracks in the 12th International Satisfiability Modulo Theories Competition.
- SMT 2017 Martin presented an extended abstract on Vampire's role as an SMT solver at the 15th International Workshop on Satisfiability Modulo Theories in Heidelberg.
- TAP 2017 Martin presented a paper on testing Vampire at the 11th International Conference on Tests & Proofs in Marburg.
- IWIL 2017 Martin presented two of our papers at the 12th International Workshop on the Implementation of Logics in Botswana.
- RV 2017 deadline approaching The deadline for submissions to RV 2017 is 1st May (abstracts 24th April). See call for papers
- CRV14 Journal Paper The paper describing the results of the first iteration of the RV competition has now been published in STTT.
- 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 Senior 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 on the Steering Committee of the RV Conference series. 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.
You can also find me on:
 |
 |
 |
 |