Master-Seminar: Quantum Computing and Formal Verification

Schedule

  • Seminar (Prof. Dr. Stefan Leue, Fabian Bauer-Marquart)
    Thursday 13:30 - 15:00        Room PZ 901         Start: 28 October 2021
  • An organizational meeting will take place on Thursday, 28 October 2021, 13:30 in PZ 901.

Description

Workload

90 hours, of which 28 hours are spent in class and 62 hours of self-study. 

Prerequisites

Master students.

Course content

Quantum computers are expected to surpass traditional computing in the not-so-distant future, potentially gaining quadratic to exponential computation speed-up. There are several state-of-the-art quantum programming languages, frameworks, and development environments that allow simulation of quantum computers, while some of them can be compiled to an instruction set architecture that runs on real quantum hardware.
While research is progressing in quantum program simulation and quantum cloud computing and quantum circuit simulation readily available, the question how to perform automated correctness proofs for quantum programs becomes more and more important. Furthermore, model checking and formal reasoning is an important means in designing quantum algorithms due to the fundamental difference to their traditional counterparts. In particular, quantum programs cannot be tested in the traditional sense because intermediate measurements can change the quantum program state.
This seminar aims at presenting approaches towards the development of formal verification technology in order to prove properties of quantum algorithms, or to test whether quantum algorithms satisfy certain properties.

Teaching methods

Learning objectives

This seminar aims at presenting approaches towards the development of formal verification technology in order to prove properties of quantum algorithms, or to test whether quantum algorithms satisfy certain properties.

Course literature

Topic 1: Robert Wille, Nils Przigoda, Rolf Drechsler:
[A Compact and Efficient SAT Encoding for Quantum Circuits](https://www.informatik.uni-bremen.de/agra/doc/konf/13_africon_sat_encoding_quantum_circuits.pdf) Africon, 2013

Topic 2: Robert Rand, Jennifer Paykin, Steve Zdancewic:
[QWIRE Practice: Formal Verification of Quantum Circuits in Coq](https://www.researchgate.net/publication/323427493_QWIRE_Practice_Formal_Verification_of_Quantum_Circuits_in_Coq/fulltext/5a9cb7e845851586a2ae35d9/QWIRE-Practice-Formal-Verification-of-Quantum-Circuits-in-Coq.pdf) QPL EPTCS 266, 2018, pp. 119–132

Topic 3: Alexandru Gheorghiu, Theodoros Kapourniotis, and Elham Kashefi:
[Verification of quantum computation: An overview of existing approaches](https://link.springer.com/content/pdf/10.1007/s00224-018-9872-3.pdf) Theory Comput Syst (2019) 63:715–808

Topic 4: Matthew Amy
[Towards Large-scale Functional Verification of Universal Quantum: Circuits](https://www.mathstat.dal.ca/~mamy/Papers/pathsum.pdf) QPL 2018. EPTCS 287, 2019, pp. 1–21

Topic 5: Timothy Atkinson, Athena Karsa, John Drake, Jerry Swan:
[Quantum Program Synthesis: Swarm Algorithms and Benchmarks](https://link.springer.com/chapter/10.1007/978-3-030-16670-0_2) EuroGP 2019, LNCS 11451, pp. 19–34, 2019.

Topic 6: Mingsheng Ying and Zhengfeng Ji:
[Symbolic Verification of Quantum Circuits](https://arxiv.org/pdf/2010.03032.pdf) arXiv, 2020

Topic 7: Christophe Chareton, Sébastien Bardin, François Bobot, Valentin Perrelle, Benoit Valiron
[A Deductive Verification Framework for Circuit-building Quantum Programs](https://arxiv.org/pdf/2003.05841.pdf) arXiv 2020

Topic 8: Kesha Hietala, Robert Rand, Shih-Han Hung, Liyi Li, Michael Hicks:
[Proving Quantum Programs Correct](https://arxiv.org/pdf/2010.01240.pdf) arXiv, 2021

Topic 9: Lukas Burgholzer, Rudy Raymond, Indranil Sengupta, Robert Wille:
[Efficient Construction of Functional Representations for Quantum Algorithms. In Conference on Reversible Computation](https://iic.jku.at/files/eda/2021_rc_efficient_construction_quantum_functionality.pdf) arXiv, 2021

Topic 10: Amira Abbas, David Sutter, Christa Zoufal, Aurelien Lucchi, Alessio Figalli, Stefan Woerner:
[The power of quantum neural networks](https://arxiv.org/pdf/2011.00027.pdf) arXiv, 2020

Target group

Master students.

Remark

The preliminary talk will take place on Thursday, 28 October 2021, 13:30 in PZ 901.

The course will be taught in English. All course materials will be in English.

Credits

ECTS 3

Weekly teaching hours

SWS 2