First Workshop on Verification of Quantum Computing (VQC 2025)

Invited Speakers

• Ross Duncan (Quantinuum)
• Aws Albarghouthi (University of Wisconsin-Madison)
• Mingsheng Ying (University of Technology Sydney)

Program

Time (UTC+2)	Event
8:30–9:00	Breakfast
9:00–9:05	Opening
Session 1
9:05–9:50	Keynote: What Should We Verify? (show abstract) Ross Duncan Verification usually means to guarantee that a computational system is correct with respect to some specification. Can this definition survive in the context of quantum computing? What parts of the system can be verified? What notions of correctness are helpful? What properties of realistic systems can be verified? What* should *we verify? I will survey the field and give some perspective on the challenges and opportunities for automated verification of quantum software. Spoiler: it's the compiler. Slides
9:50–10:10	Interval-based Analysis of Quantum Variational Computing Nicola Assolini, Luca Marzari, Isabella Mastroeni and Alessandra Di Pierro
10:10–10:30	Finding Photonics Circuits with SMT Solvers Marco Lewis and Benoît Valiron Slides
10:30–11:00	Coffee break
Session 2
11:00–11:45	Keynote: A Practical Quantum Hoare Logic with Classical Variables (show abstract) Mingsheng Ying We present a Hoare-style logic for reasoning about quantum programs with classical variables. Our approach offers several improvements over previous work: (1) Enhanced expressivity of the programming language: Our logic applies to quantum programs with classical variables that incorporate quantum arrays and parameterized quantum gates, which have not been addressed in previous research on quantum Hoare logic, either with or without classical variables. (2) Intuitive correctness specifications: In our logic, preconditions and postconditions for quantum programs with classical variables are specified as a pair consisting of a classical first-order logical formula and a quantum predicate formula (possibly parameterized by classical variables). These specifications offer greater clarity and align more closely with the programmer's intuitive understanding of quantum and classical interactions. (3) Simplified proof system: By introducing a novel idea in formulating a proof rule for reasoning about quantum measurements, along with (2), we develop a proof system for quantum programs that requires only minimal modifications to classical Hoare logic. Furthermore, this proof system can be effectively and conveniently combined with classical first-order logic to verify quantum programs with classical variables. As a result, the learning curve for quantum program verification techniques is significantly reduced for those already familiar with classical program verification techniques, and existing tools for verifying classical programs can be more easily adapted for quantum program verification. Slides
11:45–12:05	Hardware-Optimal Quantum Algorithms Stefanie Muroya, Krishnendu Chatterjee and Thomas Henzinger Slides
12:05–14:00	Lunch
Session 3
14:00–14:45	Keynote: Synthesizing Quantum Compilers (show abstract) Aws Albarghouthi The promise of quantum computing has tantalized researchers for decades, and recent breakthroughs in physical implementations have brought this technology closer to reality. However, the quantum computing landscape remains highly dynamic: competing physical substrates, fault tolerance schemes, and architectures continue to emerge with no clear frontrunner. This diversity creates a significant bottleneck in the compilation pipeline – developing and maintaining separate compilers for each new device or experimental setup is both time-consuming and error-prone. In this talk, I will present an alternative approach: automatically synthesizing device-specific quantum circuit compilers. This synthesis-based methodology enables rapid iteration while maintaining correctness guarantees. I will focus on the optimizer component, which reduces circuit size to minimize quantum computation errors. I will demonstrate how automatically synthesized optimizers can achieve superior performance compared to sophisticated hand-crafted alternatives. I will also discuss recent results on synthesizing device-specific mapping and routing algorithms. Slides
14:45–15:05	Certified Randomness from Quantum Supremacy Scott Aaronson and Shih-Han Hung
15:05–15:30	Poster Session
15:30–16:00	Coffee break
Session 4
16:00–16:20	Analysing Quantum Programs using Automata Parosh Aziz Abdulla, Yo-Ga Chen, Yu-Fang Chen, Kai-Min Chung, Lukáš Holík, Ondrej Lengal, Jyun-Ao Lin, Fang-Yi Lo, Wei-Lun Tsai and Di-De Yen Slides
16:20–16:40	On-Chip Verified Quantum Computation with an Ion-Trap Quantum Processing Unit Cica Gustiani, Dominik Leichte and Daniel Mills
16:40–17:00	Certifying Adversarial Robustness in Quantum Machine Learning: From Theory to Physical Validation Ji Guan Slides
17:00–17:30	Panel & Planning Session

Posters

• AutoQ: Automata-based Quantum Program Analyzer.
  Jyun-Ao Lin et. al.
• Barrier Certificates for Quantum Computing.
  Marco Lewis, Sadegh Soudjani and Paolo Zuliani
• Compact and Efficient Formalism for Resource and Termination Estimation in Quantum Programs.
  Jad Issa, Christophe Chareton and Romain Péchoux
• DisQ: A Model of Distributed Quantum Processors.
  Le Chang, Saitej Yavvari, Rance Cleaveland, Samik Basu and Liyi Li
  Poster
• Hybrid Programming Language for Cryptography in Rocq.
  Zhenhao Li and Li Zhou
  Poster

Organizers

• Runzhou Tao (University of Maryland)
• Yu-Fang Chen (Academia Sinica)

Program Committee

• Runzhou Tao (University of Maryland)
• Yu-Fang Chen (Academia Sinica)
• Alfons Laarman (Leiden University)
• Christophe Chareton (LORIA-CELLO)
• Ondrej Lengal (Brno University of Technology)
• Max Tschaikowski (Aalborg University)
• Nengkun Yu (Stony Brook University)
• Ji Liu (Argonne National Laboratory)
• Zichang He (JPMorgan Chase)
• Li Zhou (Max Planck Institute for Security and Privacy)
• Ferhat Erata (Yale University)