With the growing maturity of quantum computing, robust verification techniques become essential. In this paper, we introduce RuntimeSpeQ: a specification language for the runtime behaviour of quantum programs. We then propose a scheme to translate RuntimeSpeQ into runtime monitors, exploiting two types of runtime assertions. We evaluate our approach in terms of fault detection and equivalence checking capabilities as well as reusability of specifications. The results show promising runtime fault detection capabilities, with several faults detected before the final steps of the programs. Our experiments show that our monitors found 40% of faults in erroneous implementations of Quantum Phase Estimation before the final result was checked, and 90% of faults for Grover’s Algorithm. They also show no false negatives in equivalence checking. Also, across four different implementations of one case study, we found that we could reuse the same specification structure by only making minor changes, such as changing the indices pertaining to qubits or execution steps, showing the promise of reusability.
Authors: Flavio Melinte-Citea, Mohammad Reza Mousavi
Contributing partner: King's College London
