POPL 2025 (series) / CoqPL 2025 (series) / The Eleventh International Workshop on Coq for Programming Languages / Formal Verification of Quantum Stabilizer Code
Formal Verification of Quantum Stabilizer CodeRemote Participation
This project is aimed at verifying quantum error correction codes. We hope to conduct the verification in Coq, using a general approach based on the stabilizer codes. We hypothesize that by using the formalism of the stabilizer group, the efforts of verification can be reduced.
Formal Verification of Quantum Stabilizer Code Slides (Formal-Verification-of-Quantum-Stabilizer-Code-Slides.pdf) | 803KiB |
Extended Abstract (abstract.pdf) | 372KiB |
Sat 25 JanDisplayed time zone: Mountain Time (US & Canada) change
Sat 25 Jan
Displayed time zone: Mountain Time (US & Canada) change
16:00 - 17:30 | |||
16:00 22mTalk | Towards Automated Verification of LLM-Synthesized C Programs CoqPL File Attached | ||
16:22 23mTalk | CoqNFU: Towards Formalizing NFU in Coq CoqPL File Attached | ||
16:45 22mTalk | Towards Mining Robust Coq Proof PatternsRemote Participation CoqPL Cezary Kaliszyk University of Melbourne, Xuan-Bach D. Le University of Melbourne, Christine Rizkallah University of Melbourne File Attached | ||
17:07 22mTalk | Formal Verification of Quantum Stabilizer CodeRemote Participation CoqPL File Attached |