Current Projects

SCorCH: Secure Code for Capability Hardware (2020 - 2023)

This EPSRC-funded project will collaborate with the University of Oxford, Arm, and Amazon Web Services to develop formal analysis tools for a new generation of security-award hardware chips (aka capability hardware). I am the Manchester lead on the project, which is joint work with Daniel Kroening, Lucas Cordeiro, Konstantin Korovin, Pierre Olivier, and Mustafa Mustafa.

The project builds on world-leading tools and techniques in model checking, runtime verification, and automated reasoning to find security bugs in software running on CHERI/Morello chips.

See the Project Website for lots more information.


CAPS: Collaborative Architectures for Proof Search (2020 - 2022)

This EPSRC-funded project explores new collaborated architectures for automated theorem provers. The practical work of the project will be realised in the award-winning Vampire theorem prover.

The inspiration for the project is my 2015 paper on Cooperating Proof Attempts paper that shows that the AVATAR architecture for splitting can be leveraged to share information between independent proof attempts. CAPS will continue this idea to explore better ways of acheiving this and extending the sharing idea to term indexing and other parts of the architecture. The result will be a saturation-based architecture that can cooperate between proof attempts running in parallel.


QuTie: reasoning with Quantifiers and Theories (2017 - 2021)

This EPSRC-funded project, led by Andrei Voronkov, makes advances in automated theorem prover technology to reason about problems containing quantifiers and theories with a key aim of supporting program analysis.

Publications to date include:

  • Marton Hajdu, Petra Hozzová, Laura Kovacs, Johannes Schoisswohl and Andrei Voronkov: Induction with Generalization in Superposition Reasoning. CICM 2020.
  • Giles Reger, Andrei Voronkov: Induction in Saturation-Based Proof Search. CADE 2019.
  • Giles Reger, Martin Riener, Martin Suda: Symmetry Avoidance in MACE-Style Finite Model Finding. FroCos 2019.
  • Evgenii Kotelnikov, Laura Kovács, Andrei Voronkov: A FOOLish Encoding of the Next State Relations of Imperative Programs. IJCAR 2018.
  • Giles Reger, Martin Suda, Andrei Voronkov: Unification with Abstraction and Theory Instantiation in Saturation-Based Reasoning. TACAS 2018.
  • Giles Reger, Martin Suda: Set of Support for Theory Reasoning. IWIL@LPAR 2017.

Extensions implemented in Vampire during QuTie have led to success at SMT-COMP and CASC.


VyPR

This project is a collaboration with the CMS Experiment at CERN led by Joshua Dawes. VyPR is a framework that allows developers to analyse the performance of their Python programs by writing queries and analysing the results. This is all based around a specification language called Control-Flow Temporal Logic developed with Joshua.

See Project Website for further details.


Older Projects

MarQ/QEA

The Quantified Event Automata specification language and associated MarQ (Monitoring at runtime with QEA) tool was the result of my PhD and an ongoing collaboration with my supervisors Howard Barringer and David Rydeheard and collaborators Ylies Falcone and Klause Havelund. The tool is available on GitHub. I am interested in continuing this work and associated work on specification learning. There is an old project page records some work in this area.


ARVI: Runtime Verification beyond Monitoring

This was a COST Action aimed at advancing the applicability of RV. I was working group leader of the Standardization, benchmarks, tool interoperability working group. This produced a taxonomy of RV approaches and supported the ongoing development of the RV competition and accompanying benchmarks.

See Project Website for further details.