This research area aims to demonstrate the correctness of systems and covers both formal and software verification.
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.