Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Automated Verification of Silq Quantum Programs using SMT Solvers

Marco Lewis, Paolo Zuliani, Sadegh Soudjani

TL;DR

An automated tool for verifying behaviors of quantum programs written in Silq, which is a high-level programming language for quantum computing, and introduces a programming model based on a quantum RAM-style computer as an interface between Silq programs and SMT proof obligations.

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.

Automated Verification of Silq Quantum Programs using SMT Solvers

TL;DR

An automated tool for verifying behaviors of quantum programs written in Silq, which is a high-level programming language for quantum computing, and introduces a programming model based on a quantum RAM-style computer as an interface between Silq programs and SMT proof obligations.

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.
Paper Structure (29 sections, 9 equations, 8 figures, 1 table)

This paper contains 29 sections, 9 equations, 8 figures, 1 table.

Table of Contents

  1. Introduction
  2. SilVer Architecture
  3. Silq and Program Verification
  4. Quantum Computing Notation
  5. Silq and the Silq-Hybrid Fragment
  6. Program Verification using SMT Solvers
  7. Theoretical Foundations
  8. Intermediate Representation for Verification
  9. Memory
  10. Operations
  11. Instructions
  12. Controls
  13. QRAM Program Model
  14. Behavior Specification with SilSpeq
  15. Variables
  16. ...and 14 more sections

Figures (8)

  • Figure 1: SilVer Architecture
  • Figure 2: Deutsch-Jozsa Silq Program for 2 qubits. The type of $f$ states that it is a function that takes in a quantum integer and returns a boolean.
  • Figure 3: Converting a program for verification.
  • Figure 4: Reading SilSpeq specification: prog is the name of the function to be verified, input is a function input with type t1, prog_ret is the output of a function with type t2, x is a defined variable with type t3 and we have several assert statements containing logical expressions.
  • Figure 5: SilSpeq examples
  • ...and 3 more figures

Theorems & Definitions (8)

  • Definition 1
  • Remark 1
  • Definition 2
  • Definition 3
  • Definition 4
  • Definition 5
  • Definition 6
  • Example 1