No. 145 
No. 144 
No. 143 
No. 142 
No. 141 
No. 140 
No. 139 by Kim Guldstrand Larsen (Aalborg University), Christian Schilling (Aalborg University), Mirco Tribastone (IMT School for Advanced Studies Lucca), Max Tschaikowski and Paolo Zuliani (Sapienza University of Rome)
Techniques developed to analyze classical software are finding a new role in quantum computing. Our recent work shows how model reduction, model checking and satisfiability solving can help simulate quantum programs and verify quantum communication protocols.
Quantum computing is often discussed as a hardware race: more qubits, lower error rates and longer coherence times. But useful quantum computers will also need a mature software stack. Programmers must be able to describe algorithms at a convenient level, simulate them before execution and gain confidence that the resulting software does what it is supposed to do.
Quantum software makes this particularly challenging. A classical program can be paused and inspected. A quantum state, by contrast, cannot simply be read without changing what happens next, and access to real quantum hardware remains limited. This makes conventional testing difficult.
This is where formal methods can help. Formal methods are mathematical and algorithmic techniques for analyzing software and systems, developed over decades for areas such as embedded systems, communication protocols and safety-critical software. Our vision is to transfer these techniques between research communities and bring them into quantum computing rather than starting the quantum software toolbox from scratch.
This direction is central to the Danish ODAQS project, which brings together Aarhus University, Aalborg University and the quantum-software company Kvantify. ODAQS develops a software stack spanning compilation, simulation and verification, with computational chemistry as a major application area. The vision is shared by the Italian project QUMOBA at the Sapienza University of Rome, which develops scalable methods for verifying quantum circuits by combining model reduction with barrier certificates.
The broader agenda also includes CLASSIQUE, the Center for Classical Communication in the Quantum Era at Aalborg University. CLASSIQUE is funded by the Danish National Research Foundation with about EUR 12 million. Its research includes reliability and verification for systems combining classical and quantum communication.
Building a community around this transfer is equally important. In 2025, we initiated the Workshop on Formal Methods in Quantum Computing (FMQC) [L1]. It brings together researchers from quantum computing and formal methods and encourages the exchange of methods between the two communities. A second edition was held in Lisbon in 2026, and a third is planned for 2027 in Copenhagen.
What can this transfer look like in practice? Three recent results illustrate the idea. Figure 1 summarizes this technology transfer from formal methods to quantum computing.
First, a quantum system with only a modest number of qubits already has an enormous classical state space, so simulation quickly becomes expensive. In [1], we adapted a formal-methods technique called bisimulation, traditionally used to identify states that behave in the same way. The method searches for a smaller representation of a quantum computation while preserving the information that matters for the result. Combined with efficient data structures called decision diagrams, this produced speed-ups of several orders of magnitude on quantum-circuit benchmarks, including established algorithms for search and optimization. For Grover's search algorithm, the dynamics can even be reduced to a two-state description while preserving the relevant outcome.
Second, formal methods can help with quantum communication. In [2], we extended the verification tool UPPAAL, originally developed for classical real-time systems, so that it can analyze protocols containing quantum states, operations and measurements. The approach was applied to a two-way quantum communication protocol together with entanglement distillation. UPPAAL can exhaustively check ideal, noiseless versions and use so-called statistical model checking when realistic timing and noise are included. This matters because future quantum networks will combine classical control, timing constraints and fragile quantum resources.
Third, we can borrow automatic reasoning technology from software verification. In [3], the tool symQV translates the question "does this quantum program satisfy its specification?" into mathematical constraints handled by a so-called satisfiability modulo theory (SMT) solver. Such solvers are widely used in formal verification and model checking.
These examples use different techniques, but the message is the same. Quantum computing creates genuinely new challenges, yet many surrounding software problems - reducing complex systems, checking protocol behavior and proving program correctness - have close classical relatives. Decades of research in formal methods therefore provide a rich source of ideas, algorithms and mature tools.
The next step is to make these techniques part of everyday quantum software engineering. ODAQS, QUMOBA and CLASSIQUE pursue this goal, while FMQC provides a meeting place for the communities whose ideas need to come together. The ambition is not to make quantum computing classical. It is to make quantum technology benefit from what computer science already knows about building software that is efficient, predictable and trustworthy.
Link:
[L1] https://fmqc-workshop.github.io/2025/
References:
[1] L. Burgholzer, et al., “Forward and Backward Constrained Bisimulations for Quantum Circuits Using Decision Diagrams”, ACM Transactions on Quantum Computing 6(2), 2025. DOI: 10.1145/3712711
[2] R. Bødker Christensen, et al., “Analysis and Verification of Quantum Communication Protocols in UPPAAL”, CAV 2026, 2026. DOI: 10.1007/978-3-032-32537-2_18
[3] F. Bauer-Marquart, S. Leue, and C. Schilling, “symQV: Automated Symbolic Verification of Quantum Programs”, FM 2023, 2023. DOI: 10.1007/978-3-031-27481-7_12
Please contact:
Kim Guldstrand Larsen
Aalborg University, Denmark
Max Tschaikowski
Sapienza University of Rome, Italy