Automated Verification of Silq Quantum Programs using SMT Solvers

TL;DR

This paper introduces SilVer, an automated verification tool for Silq quantum programs that uses SMT solvers to ensure correctness against user specifications, integrating a quantum RAM model and measurement-based conditions.

Contribution

It presents a novel verification framework combining a quantum RAM model with SMT solvers for high-level quantum program correctness assurance.

Findings

Successfully verified entangled state generation

Verified multiple oracle-based quantum algorithms

Demonstrated effectiveness on real-world quantum programs

Abstract

We present SilVer (Silq Verification), an automated tool for verifying behaviors of quantum programs written in Silq, which is a high-level programming language for quantum computing. The goal of the verification is to ensure correctness of the Silq quantum program against user-defined specifications using SMT solvers. We introduce a programming model that is based on a quantum RAM-style computer as an interface between Silq programs and SMT proof obligations, allowing for control of quantum operations using both classical and quantum conditions. Additionally, users can employ measurement flags within the specification to easily specify conditions that measurement results require to satisfy for being a valid behavior. We provide case studies on the verification of generating entangled states and multiple oracle-based algorithms.