Concurrent Quantum Separation Logic for Fine-Grained Parallelism

This conference talk presents a novel concurrent quantum separation logic for verifying fine-grained parallelism in quantum computing. Learn how researchers Yusuke Matsushita, Kengo Hirata, and Ryo Wakizaka from Kyoto University and the University of Edinburgh address the challenge of modularly verifying correctness in parallel quantum subroutines. Discover their innovative approach featuring new proof rules for linearly combining Hoare triples and fractional tokens that enable sharing qubits between parallel operations. The presentation demonstrates the effectiveness of this logic by verifying a complex parallelized quantum program. The talk was delivered at the Theory and Practice of Static Analysis workshop (TPSA'25) on January 21, 2025, sponsored by ACM SIGPLAN.