Area of investment and support

Verification and correctness

This research area aims to demonstrate the correctness of systems and covers both formal and software verification.

• Partners involved: Engineering and Physical Sciences Research Council (EPSRC)

The scope and what we're doing

This area aims to demonstrate the correctness of systems and contributes to software and hardware co-design.

Formal verification aims to establish that the design of a system and its underlying algorithms are correct with respect to a formal specification. Software verification assesses how well software satisfies defined requirements.

Both forms of verification include evaluation of properties such as performance, safety and security.

The strategy for this area recognises that verification and correctness research in the UK is of high quality and very strong in international standing.

Our goal is to create a portfolio of research that tackles the challenges posed by more complex, distributed, large-scale systems and builds on existing links with other research areas, such as Artificial Intelligence Technologies, ICT Networks and Distributed Systems, and Theoretical Computer Science.

This includes contributing to EPSRC’s Future Intelligent Technologies priority for the ICT theme, particularly in terms of the development of trusted technologies.

We want to strengthen our researchers’ existing links between theory and practice to address real-world challenges, including the development of usable tools. We also aim for consideration of human interaction with verification technologies to take place from the outset, in line with EPSRC’s People at the Heart cross-ICT priority.

Researchers addressing cybersecurity challenges and contributing to ongoing work driven by security issues. The involvement of verification and correctness researchers is integral to realising the aims of EPSRC’s Safe and Secure cross-ICT priority by ensuring reliable, robust systems that can cope in a modern, complex world.

In recognition of the increased interest from industry in verification and correctness, we will monitor the supply of people into the relevant research community.

Why we're doing it

The UK is a recognised leader across the spectrum of work funded in this area, from formal to software verification. This is demonstrated by a strong international profile and representation at key conferences.

There are several world leading groups and individuals in the UK, highlighted by a number of programme grants and fellowships and significant investment from other funders, including European Research Council grant holders, providing significant capacity in this area.

Work in this research area most often overlaps with Software Engineering and researchers often span the two. There are also strong links with Theoretical Computer Science.

Engagement with the academic and user community has identified that verification and correctness has the greatest potential to contribute to the most significant research challenges in cybersecurity over the next five to ten years.

With the world moving to complex, open, large-scale systems and environments, there are new opportunities for verifying systems and their interactions in a practical way. These include autonomous systems, safety-critical systems, the ‘internet of things’ and quantum computing.

The verification of systems and their behaviour is an important consideration as part of responsible innovation and has an impact in the fields of regulation and certification. There have been a number of successful spin outs from UK-based research groups (for example, Monoidics) and large organisations (for example, Facebook and Amazon) now have verification teams based in the UK. This is creating demand for trained people, suggesting that this research area is meeting an important need in the UK.

The link between hardware and software verification continues to be a UK strength, with companies such as ARM and Microsoft having good links with the research community.

The student population funded by ICT is reasonably balanced between the doctoral training partnership and centres for doctoral training, with some industrial collaborative awards in science and engineering studentships as well.

View evidence sources used to inform our research strategies.

Past projects, outcomes and impact

Visualising our portfolio (VoP) is a tool for users to visually interact with the EPSRC portfolio and data relationships. Find out more about research area connections and funding for Verification and Correctness.

Find previously funded projects on Grants on the Web.

Last updated: 6 January 2023