Verification of Quantum Processes in a Functional Based Programming Language

Tiancheng Jin, Jianjun Zhao

Ensuring the correctness of quantum programs is crucial for quantum software quality assurance. Although various effective verification methods exist for classical programs, they cannot be applied to quantum programs due to the fundamental differences in their execution logic, such as quantum superposition and entanglement. This calls for new methods to verify the correctness of quantum programs. In this paper, we present a behavioral interface specification language (BISL) called ScaffML for the quantum programming language Scaffold. ScaffML allows the specification of pre- and post-conditions for Scaffold modules and enables the mixing of assertions with Scaffold code, thereby facilitating debugging and verification of quantum programs. This paper discusses the goals and overall approach of ScaffML and describes the basic features of the language through examples. ScaffML provides an easy-to-use specification language for quantum programmers, supporting static analysis, run-time checking, and formal verification of Scaffold programs. Finally, we present several instances to illustrate the workflow and functionalities of ScaffML.

Mingsheng Ying, Nengkun Yu, Yuan Feng +1 more

Mingsheng Ying

Kesha Hietala, Rand, Robert, Shih-Han Hung +2 more

We present sqire, a low-level language for quantum computing and verification. sqire uses a global register of quantum bits, allowing easy compilation to and from existing `quantum assembly' languages and simplifying the verification process. We demonstrate the power of sqire as an intermediate representation of quantum programs by verifying a number of useful optimizations, and we demonstrate sqire's use as a tool for general verification by proving several quantum programs correct.

Yoshihiko Kakutani

Ji Guan, Mingsheng Ying, Runyao Duan +3 more

This paper describes a quantum programming environment called $Q|SI\rangle $ . It is a platform created in the .NET language to support quantum programming as a quantum extension of the $\mathbf{while}$-language. This platform includes a compiler for the quantum $\mathbf{while}$-language and a chain of tools for the simulation of quantum computations, optimization of quantum circuits, and analysis and verification of quantum programs. Throughout the paper, $Q|SI\rangle $ is used to simulate quantum behaviors on classical platforms and demonstrate the combination of components. The scalable framework allows users to program customized functions on the platform. The compiler works as the core of $Q|SI\rangle $ , bridging the gap between quantum hardware and quantum software. The built-in decomposition algorithms enable universal quantum computation on current quantum hardware.