SPLASH 2025
Sun 12 - Sat 18 October 2025 Singapore
co-located with ICFP/SPLASH 2025

This program is tentative and subject to change.

Sat 18 Oct 2025 11:30 - 11:45 at Orchid Small - Quantum

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 Oct

Displayed time zone: Perth change

10:30 - 12:15
10:30
15m
Talk
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
15m
Talk
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
15m
Talk
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
15m
Talk
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
15m
Talk
QbC: Quantum Correctness by Construction
OOPSLA
Anurudh Peduri Ruhr University Bochum, Ina Schaefer KIT, Michael Walter Ruhr-Universität Bochum
11:45
15m
Talk
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
15m
Talk
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