Advancing Quantum Computing with Formal Methods

Lecture notes in computer science, pp. 420–446

Abstract

Abstract This tutorial introduces quantum computing with a focus on the applicability of formal methods in this relatively new domain. We describe quantum circuits and convey an understanding of their inherent combinatorial nature and the exponential blow-up that makes them hard to analyze. Then, we show how weighted model counting (#SAT) can be used to solve hard analysis tasks for quantum circuits. This tutorial is aimed at everyone in the formal methods community with an interest in quantum computing. Familiarity with quantum computing is not required, but basic linear algebra knowledge (particularly matrix multiplication and basis vectors) is a prerequisite. The goal of the tutorial is to inspire the community to advance the development of quantum computing with formal methods.

Authors 4

1. Arend-Jan Quist Aachen

   Leiden University

   Affiliation as printed

   Leiden University, Leiden, The Netherlands

2. Jingyi Mei Aachen

   Leiden University

   Affiliation as printed

   Leiden University, Leiden, The Netherlands

3. Tim Coopmans corresponding Aachen

   Leiden University

   Affiliation as printed

   Leiden University, Leiden, The Netherlands

4. Alfons Laarman Aachen

   Leiden University

   Affiliation as printed

   Leiden University, Leiden, The Netherlands