5 papers
SAT, MaxSAT, and SMT for QLDPC Distance Computation: A Large-Scale Empirical Study
Yu-Fang Chen, Seyed Mohammad Reza Jafari, Ching-Yi Lai
Exact distance computation for quantum LDPC (QLDPC) codes plays a central role in validating candidate fault-tolerant quantum-code constructions, yet the computational structure of…
A Practical Specification Language for Automatic Quantum Program Verification (Technical Report)
Wei-Lun Tsai, Yu-Fang Chen, OndÅej Lengál
Hoare-style verification provides a principled foundation for reasoning about the correctness of quantum programs, but existing approaches do not allow fully automatic verification…
AutoQ 2.0: From Verification of Quantum Circuits to Verification of Quantum Programs (Technical Report)
Yu-Fang Chen, Kai-Min Chung, Min-Hsiu Hsieh +4
We present a verifier of quantum programs called AutoQ 2.0. Quantum programs extend quantum circuits (the domain of AutoQ 1.0) by classical control flow constructs, which enable us…
Equivalence Checking of Quantum Circuits via Path-Sum and Weighted Model Counting
Wei-Jia Huang, Christophe Chareton, Yu-Fang Chen +4
Equivalence checking of quantum circuits is a central verification task in quantum computing, ensuring the correctness of circuit optimizations, hardware mappings, and compilation…
Parameterized Verification of Quantum Circuits (Technical Report)
Parosh Aziz Abdulla, Yu-Fang Chen, Michal HeÄko +4
We present the first fully automatic framework for verifying relational properties of parameterized quantum programs, i.e., a program that, given an input size, generates a corresp…