Verified Simulation for Large Quantum Systems (VSL-Q)
Lead Research Organisation:
King's College London
Department Name: Informatics
Abstract
Programming classical computers has become a popular practice thanks to high-level programming languages and compilers which enable the running
of high-level programs on different computing platforms. For critical applications, we now have verified compilation schemes and certified
compilers which ensure the correctness of the compiled executions. This is done by reference to a mathematical model of the high-level code. In
this project we will establish such a promising trajectory for quantum computing, taking into account the subtle features of quantum computers.
This will be achieved by bringing together expertise in software testing and quantum simulation. The results of this research will lead to verified software for quantum computing applications and consequently, to wide-spread and effective exploitation of quantum computing.
of high-level programs on different computing platforms. For critical applications, we now have verified compilation schemes and certified
compilers which ensure the correctness of the compiled executions. This is done by reference to a mathematical model of the high-level code. In
this project we will establish such a promising trajectory for quantum computing, taking into account the subtle features of quantum computers.
This will be achieved by bringing together expertise in software testing and quantum simulation. The results of this research will lead to verified software for quantum computing applications and consequently, to wide-spread and effective exploitation of quantum computing.
Publications
Abeywickrama D
(2023)
On Specifying for Trustworthiness
in Communications of the ACM
Aceto L
(2023)
The Way We Were: Structural Operational Semantics Research in Perspective
in Electronic Proceedings in Theoretical Computer Science
Barbanera F
(2023)
Multicompatibility for Multiparty-Session Composition
Barwell A D
(2023)
Designing Asynchronous Multiparty Protocols with Crash-Stop Failures
Bensoussan, A.
(2025)
A Taxonomy of Real Faults in Hybrid Quantum-Classical Architectures
D'Aloisio G
(2024)
Exploring LLM-Driven Explanations for Quantum Algorithms
Fortz S
(2024)
VaryMinions: leveraging RNNs to identify variants in variability-intensive systems' logs
in Empirical Software Engineering
Gheri L
(2023)
Hybrid Multiparty Session Types: Compositionality for Protocol Specification through Endpoint Projection
in Proceedings of the ACM on Programming Languages
Heuvel B
(2024)
Typed Non-determinism in Concurrent Calculi: The Eager Way
in Electronic Notes in Theoretical Informatics and Computer Science
Hierons R.
(2025)
Complete FSM Testing Using Strong Separability
| Description | We started off by laying a rigorous fundation to testing quantum systems; we performed investigations both at the theoretical level, using testing theories available from process calculi, and at the practical level by studying the extensions of property-based testing and debugging tools. On both fronts, we found that extending testing and debugging methods to the quantum (and hybrid quantum-classical) setting is challenging and requires substantial effort. We have taken on this challenge and produced the first editions of property-based testing and debugging tools for fault tolerant quantum computing. We intend to extend these results to noisy architectures and hybrid quantum-classical systems. |
| Exploitation Route | The outcomes have just been released; they have been disseminated to some extent, e.g., in the recent keynote and guest lectures by the PI, but we need more time to report on impact. |
| Sectors | Digital/Communication/Information Technologies (including Software) |
| Description | We have been engaging with a wide range of stakeholders, through academic keynotes, guest lectures, podcasts, and YouTube videos. We have been engaging with our industrial and academic partners (e.g., BT and Simula Labs) and have hosted researchers from leading international institutions (CNR, Italy; Simula Labs, Norway; University of Oslo, Norway; University of Sao Paolo, Brazil). Our public engagement activities have received substantial attention (more than 57k views of our YouTube episode) and we have embarked upon new industrial collaborations involving a dozen of new partners. |
| First Year Of Impact | 2025 |
| Sector | Digital/Communication/Information Technologies (including Software),Financial Services, and Management Consultancy |
| Impact Types | Economic Policy & public services |
| Description | Scalable Quantum Network Technologies: Collaborative R&D |
| Amount | £1,972,000 (GBP) |
| Organisation | Innovate UK |
| Sector | Public |
| Country | United Kingdom |
| Start | 03/2024 |
| End | 10/2025 |
| Description | Noise-Aware Testing of Large-Scale Quantum Systems, Simula Research Labs, Oslo |
| Organisation | Simula Research Laboratory |
| Country | Norway |
| Sector | Academic/University |
| PI Contribution | We established a strategic research collaboration with Simula Research Labs in Oslo, Norway on noise-aware testing techniques for large-scale quantum systems. This has led to mutual visits (both undertaken and planned) and planned joint research and publications. |
| Collaborator Contribution | Our partners shared their datasets and code for noise-aware testing of quantum systems and in return, we provided properties and code developed in our past research. We are integrating the bodies of knowledge, techniques and tools, to provide a comprehensive noise-aware framework for testing large-scale quantum systems. |
| Impact | Not applicable (yet). |
| Start Year | 2023 |
| Description | Unified Framework for Hybrid Quantum-Classical Systems, Quantum Hub, University of Copenhagen |
| Organisation | University of Copenhagen |
| Country | Denmark |
| Sector | Academic/University |
| PI Contribution | Mohammad Reza Mousavi delivered a lecture in the hybrid quantum-classical computing course at the University of Copnehagen. As a result of the lecture and the visit, we planned a long-term mutual collaboration. We have now submitted an outline proposal to the Danish research funding agency. |
| Collaborator Contribution | Guest lecture Planned collaboration |
| Impact | Delivered a guest lecture; planned a formal research collaboration. Outcomes to be posted in subsequent reports. |
| Start Year | 2025 |
| Title | QuCheck: A Property-based Testing Framework for Quantum Programs in Qiskit |
| Description | We present QuCheck, a property-based testing framework for Qiskit quantum programs. |
| Type Of Technology | Software |
| Year Produced | 2024 |
| Open Source License? | Yes |
| Impact | Just published; the predecessor to this tool, called QSharpCheck, has been cited about 100 times and has been used in many subsequent research activities. |
| URL | https://figshare.com/articles/software/QuCheck_A_Property-based_Testing_Framework_for_Quantum_Progra... |
| Description | Computerphile YouTube Episode on Quantum Software Engineering |
| Form Of Engagement Activity | A broadcast e.g. TV/radio/film/podcast (other than news/press) |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Public/other audiences |
| Results and Impact | I produced an episode of Computerphile on Quantum Software Engineering. The episode has been viewed more than 57,000 times to date. |
| Year(s) Of Engagement Activity | 2025 |
| URL | https://www.youtube.com/watch?v=l909v-D8Z0s |
| Description | INGI lunchtime seminar |
| Form Of Engagement Activity | A talk or presentation |
| Part Of Official Scheme? | No |
| Geographic Reach | Local |
| Primary Audience | Postgraduate students |
| Results and Impact | I was invited as the speaker for the INGI Lunchtime Seminar on October 3, 2024, at the Computing Science and Engineering Department (INGI) of UCLouvain, Belgium. These seminars, held twice a month, cover various topics in computing sciences and are open to all audiences. |
| Year(s) Of Engagement Activity | 2024 |
| Description | Medicine, Life Sciences, and Quantumhow do we join the dots? |
| Form Of Engagement Activity | Participation in an activity, workshop or similar |
| Part Of Official Scheme? | No |
| Geographic Reach | National |
| Primary Audience | Professional Practitioners |
| Results and Impact | We organised a workshop with about 40 participants ranging from policy makers (such as DSIT), funders (such as MRC and NIHR), healthcare professionals and companies to discuss the possibilities of using quantum computing and sensing in the healrthcare domain. The event led to many follow up plans for joint activities. |
| Year(s) Of Engagement Activity | 2025 |
| URL | https://www.eventbrite.co.uk/e/medicine-life-sciences-and-quantumhow-do-we-join-the-dots-tickets-108... |
| Description | Quantum Computing for Healthcare Engineering |
| Form Of Engagement Activity | Participation in an activity, workshop or similar |
| Part Of Official Scheme? | No |
| Geographic Reach | Local |
| Primary Audience | Professional Practitioners |
| Results and Impact | We held a workshop explaining the principles of quantum computing and the available practical frameworks (e.g., for quantum annealing, variational quantum algorithms and quantum machine learning) to healthcare professionals at the London Institute for Healthcare Engineering. We also reviewed the recent application of such techniques in the healthcare domain. The event was recorded and was provided as preliminary material to the larger group of participants in the subsequent event in March. |
| Year(s) Of Engagement Activity | 2025 |
| URL | https://www.eventbrite.co.uk/e/quantum-computing-for-healthcare-engineering-tickets-1106292032249?af... |
| Description | Quantum Demystified Podcast |
| Form Of Engagement Activity | Engagement focused website, blog or social media channel |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Public/other audiences |
| Results and Impact | We planned and so far delivered four episodes of the Quantum Demystified Podcast. They discuss the general landscape of quanrtum technologies and specifically discuss applications in healthcare. Moreover, we discuss the foundations and applications of superposition and entangelemtn in quantum computing. All episodes feature speakers across different disciplines (involving chemists, computer scientists, philosophers, physicists, and biologists) and are designed to be accessible for the general public. |
| Year(s) Of Engagement Activity | 2024,2025 |
| URL | https://www.buzzsprout.com/2318723 |
| Description | Seminar for the *Actuality in Data Science* Course |
| Form Of Engagement Activity | A talk or presentation |
| Part Of Official Scheme? | No |
| Geographic Reach | Local |
| Primary Audience | Postgraduate students |
| Results and Impact | Two-hour seminar for the *Actuality in Data Science* course at the University of Namur (Belgium), attended by first-year master's students and several academic colleagues. The seminar covered an introduction to quantum programming and mutation testing, a summary of achievements in the VSL-Q project, and an overview of my early research findings. |
| Year(s) Of Engagement Activity | 2024 |
| URL | https://www.unamur.be/en/actualites-en-data-science |