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