Automated Formal Verification of Quantum Protocols for the Quantum Era

Research Project

Project/Area Number	24K20757
Research Category	Grant-in-Aid for Early-Career Scientists
Allocation Type	Multi-year Fund
Review Section	Basic Section 60050:Software-related
Research Institution	Japan Advanced Institute of Science and Technology
Principal Investigator	DO CanhMinh 北陸先端科学技術大学院大学, 先端科学技術研究科, 助教 (00981143)
Project Period (FY)	2024-04-01 – 2027-03-31
Project Status	Granted (Fiscal Year 2024)
Budget Amount *help	¥2,730,000 (Direct Cost: ¥2,100,000、Indirect Cost: ¥630,000) Fiscal Year 2026: ¥650,000 (Direct Cost: ¥500,000、Indirect Cost: ¥150,000) Fiscal Year 2025: ¥650,000 (Direct Cost: ¥500,000、Indirect Cost: ¥150,000) Fiscal Year 2024: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
Keywords	Dynamic Quantum Logic / Quantum Protocols / Concurrency / Algebraic Specification / Maude
Outline of Research at the Start	This research project aims to develop automated formal verification of quantum protocols based on Dynamic Quantum Logic (DQL). This project will contribute to the reliability of quantum protocols and advance the development of DQL and its applications in automated quantum protocol verification.