[CPP'26] Specification, Semantics, and Verification of Quantum Programs скачать в хорошем качестве

[CPP'26] Specification, Semantics, and Verification of Quantum Programs

Specification, Semantics, and Verification of Quantum Programs (Video, CPP 2026) Jennifer Paykin (University of Vermont) Abstract: One of the central questions of formal verification asks: does this program do what it’s supposed to? Built into this simple idea are more subtle underlying questions: How do we precisely specify a program’s intended behavior? How do we formally reason about what the program actually does? And how do we rigorously and efficiently verify that these two notions align? In the interdisciplinary field of quantum computing, answering these questions requires particular nuance. Researchers from different backgrounds bring different perspectives on both specification and analysis. A quantum program’s specification can be expressed as a probability distribution over measurement results, as a complex matrix of exponential size, or as an abstract categorial diagram. A program’s semantics can be described by an idealized step relation, or more realistically, can incorporate noise models, decoherence, and the physical constraints of state-of-the-art quantum computing hardware. This talk will explore what it means for a quantum program to “do what it’s supposed to”: how to specify correctness; how to analyze actual behavior; and how formal verification can bridge the gap between them. Luckily, we can draw on a rich toolbox of classical formal methods, including equivalence checking, program logics, and compiler correctness to verify these quantum programs. In this talk I will survey the landscape of quantum program verification, highlight emerging approaches, and identify open problems. This talk is designed to be accessible to a general audience; no prior background in quantum computing is expected. Presentation at the CPP 2026 conference, Jan 12-13, 2026, https://popl26.sigplan.org/home/CPP-2... Sponsored by ACM SIGPLAN.