Verification and correctness

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.

We aim to maintain this research area as a proportion of the EPSRC portfolio. This strategy recognises that Verification and Correctness research in the UK is of high quality and very strong in international standing.

By the end of the current Delivery Plan period, our goal is to have:

  • 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
  • Researchers strengthening 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 cyber-security 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.

Highlights:

The UK is a recognised leader across the spectrum of work funded in this area, from formal to software verification - 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 (Evidence source 1) and significant investment from other funders, including a number of ERC 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 cyber-security over the next five to ten years (Evidence source 2,3).

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 impact in the fields of regulation and certification. There have been a number of successful spinouts from UK-based research groups (e.g. Monoidics) and large organisations (e.g. 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 (DTP) and Centres for Doctoral Training (CDTs), with some Industrial Collaborative Awards in Science and Engineering (CASE) studentships as well (Evidence source 1).

This area will contribute to all Outcomes but most strongly to the Connected and Resilient Nation over a shorter timeframe. The following Ambitions are of particular note:

C4: Ensuring a safe and trusted cyber society

This research area can enable development of trusted tools and foundational techniques.

R3: Develop better solutions to acute threats: cyber, defence, financial and health

Advances in this research area will be needed to anticipate and adapt to acute threats in complex systems.

  1. Analysis of EPSRC application and student data.
  2. Community engagement (individual input, group feedback, team visits and evidence-gathering) and input from the ICT Strategic Advisory Team, the UK Computing Research Council (UKCRC) Executive Committee and Research Excellence Framework (REF) 2014 panellists (sub-panel 11).
  3. Research Institute in Automated Program Analysis and Verification, Annual Report, (2015).

Research area connections

This diagram shows the top 10 connections between Research Areas within the EPSRC research portfolio. The depth of the segment relates to value of grants and the width of the segment relates to the number of grants shared by those two Research Areas. Please click to see the related Research Area rationale.

Maintain

We aim to maintain this area as a proportion of the EPSRC portfolio.

Visualising our Portfolio (VoP)
Visualising our portfolio (VoP) is a tool for users to visually interact with the EPSRC portfolio and data relationships.

EPSRC Support by Research Area in Verification and Correctness (GoW)
Search EPSRC's research and training grants.

Contact Details

In the following table, contact information relevant to the page. The first column is for visual reference only. Data is in the right column.

Name: Michael Barclay
Job title: Portfolio Manager
Organisation: EPSRC
Telephone: 01793 444544