QbC: Quantum Correctness by Construction
This program is tentative and subject to change.
Thanks to the rapid progress and growing complexity of quantum algorithms, correctness of quantum programs has become a major concern. Pioneering research over the past years has proposed various approaches to formally verify quantum programs using proof systems such as quantum Hoare logic. All these prior approaches are post-hoc: one first implements a program and only then verifies its correctness. Here we propose \emph{Quantum Correctness by Construction (QbC)}: an approach to constructing quantum programs from their specification in a way that ensures correctness. We use pre- and postconditions to specify program properties, and propose sound and complete refinement rules for constructing programs in a quantum while language from their specification. We validate QbC by constructing quantum programs for idiomatic problems and patterns. We find that the approach naturally suggests how to derive program details, highlighting key design choices along the way. As such, we believe that QbC can play a role in supporting the design and taxonomization of quantum algorithms and software.
This program is tentative and subject to change.
Sat 18 OctDisplayed time zone: Perth change
10:30 - 12:15 | |||
10:30 15mTalk | AccelerQ: Accelerating Quantum Eigensolvers With Machine Learning on Quantum Simulators OOPSLA Avner Bensoussan King's College London, Elena Chachkarova Kings College London, Karine Even-Mendoza King’s College London, Sophie Fortz King's College London, Connor Lenihan King's College London | ||
10:45 15mTalk | A Language for Quantifying Quantum Network Behavior OOPSLA Anita Buckley USI Lugano, Pavel Chuprikov Télécom Paris, Institut Polytechnique de Paris, Rodrigo Otoni USI Lugano, Robert Soulé Yale University, Robert Rand University of Chicago, Patrick Eugster USI Lugano, Switzerland | ||
11:00 15mTalk | Compositional Quantum Control Flow with Efficient Compilation in Qunity OOPSLA Mikhail Mints California Institute of Technology, Finn Voichick University of Maryland, Leonidas Lampropoulos University of Maryland, College Park, Robert Rand University of Chicago | ||
11:15 15mTalk | Dependency-Aware Compilation for Surface Code Quantum Architectures OOPSLA Abtin Molavi University of Wisconsin-Madison, Amanda Xu University of Wisconsin-Madison, Swamit Tannu University of Wisconsin-Madison, Aws Albarghouthi University of Wisconsin-Madison | ||
11:30 15mTalk | QbC: Quantum Correctness by Construction OOPSLA | ||
11:45 15mTalk | qblaze: An Efficient and Scalable Sparse Quantum Simulator OOPSLA Hristo Venev INSAIT, Sofia University "St. Kliment Ohridski", Thien Udomsrirungruang University of Oxford, Dimitar Dimitrov INSAIT, Sofia University "St. Kliment Ohridski", Timon Gehr ETH Zurich, Martin Vechev ETH Zurich | ||
12:00 15mTalk | Shaking Up Quantum Simulators with Fuzzing and Rigour OOPSLA Vasileios Klimis Queen Mary University of London, Karine Even-Mendoza King’s College London, Avner Bensoussan King's College London, Elena Chachkarova Kings College London, Sophie Fortz King's College London, Connor Lenihan King's College London |