Building a trustworthy quantum era through formal verification

Laboratory on Formal Methods for Quantum Computing
Senior Lecturer：DO Minh Canh

E-mail：
［Research areas］
Formal Methods, Quantum Computing
［Keywords］
Formal Specification, Model Checking, Theorem Proving, Quantum Computation, Quantum Information

Skills and background we are looking for in prospective students

We welcome highly motivated students with an interest in formal methods and quantum computing, a good knowledge of mathematics (especially mathematical logic and linear algebra), and strong programming skills (C++, Java, Python).

What you can expect to learn in this laboratory

In our laboratory, students will learn how to formalize quantum systems as state machines; how to specify state machines in a formal specification language, such as Maude or CafeOBJ; and how to formally verify that state machines enjoy desired properties using model checking and/or theorem proving techniques. Through these research activities, students are expected to become independent researchers with a solid theoretical foundation, advanced practical skills, and a passion for advancing both conventional and quantum technologies in ways that benefit society.

【Job category of graduates】 Researcher & Engineer

Research outline

With recent exponential investments from governments and major companies, building large-scale quantum computers capable of running advanced algorithms, such as Shor’s algorithm for effectively solving the factoring and discrete logarithm problems, is only a matter of time and effort. Despite its promise, quantum computing is fundamentally different from classical computing because it relies on the unique principles of quantum mechanics, such as superposition, entanglement, and measurement, which are often counterintuitive and make it challenging to design and implement quantum algorithms, programs, and protocols accurately. Therefore, formal verification is essential to ensure their correctness before they can be trusted in safety-critical and security applications. Our current research focuses on formal methods for quantum computing, including but not limited to the following research topics.

A unified, expressive, and scalable framework for formal specification and verification of quantum systems

This framework will introduce a powerful formal specification language capable of modeling a wide range of quantum systems, including those with concurrency and classical-quantum communication, along with scalable formal verification techniques ranging from model checking to theorem proving.
Our research group has proposed Concurrent Dynamic Quantum Logic (CDQL) as a logical framework that can be used to specify concurrent behavior and communication among participants. In addition, we have developed a Maude-based tool with a lazy rewriting strategy that automates the entire verification process and effectively handles the vast number of interleavings with communication arising from concurrency.

A verifiable recursive quantum programming language with formal semantics

This recursive quantum programming language will provide a modular approach to designing quantum systems and verifying them rigorously with formal methods grounded in its formal semantics, while retaining the unique advantages of quantum computing.
Our research group has proposed the syntax and operational semantics for recursive quantum programming that support unitary operations, measurements, conditional statements, loop statements, atomic statements, and recursive procedure calls. Building on this foundation, we have developed a framework for specifying quantum programs within the scope of the proposed language and automatically verifying their correctness through reachability analysis.

Key publications

1. Canh Minh Do, Adrián Riesco, Santiago Escobar, Kazuhiro Ogata. “Parallel Maude-NPA for Cryptographic Protocol Analysis”, IEEE Transactions on Dependable and Secure Computing, IEEE, 2025. (To Appear)
2. Canh Minh Do, Tsubasa Takagi, Kazuhiro Ogata. “Automated Quantum Protocol Verification Based on Concurrent Dynamic Quantum Logic”, ACM Transactions on Software Engineering and Methodology, 34(6): 1-36, ACM, 2025.
3. Canh Minh Do, Yati Phyo, Adrián Riesco, Kazuhiro Ogata. “Optimization Techniques for Model Checking Leads-to Properties in a Stratified Way”, ACM Transactions on Software Engineering and Methodology, 32(6): 1-38, ACM, 2023.

Equipment

Maude (a rewriting logic-based specification/programming language)
CafeOBJ (an advanced formal specification and verification language)
MacPros (a high-performance computing environment for experiments)