activity
20242026
most citedEquivalence Checking of Quantum Circuits via Path-Sum and Weighted Model Counting

2 citations · 3 across the 4 of their papers we have counts for

collaborators

6 papers

quant-ph2026

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…

cs.LO2026

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…

cs.LO20261 cited

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…

cs.SC20262 cited

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…

cs.LO2025

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…

cs.LO2024

Verifying Quantum Circuits with Level-Synchronized Tree Automata (Technical Report)

Parosh Aziz Abdulla, Yo-Ga Chen, Yu-Fang Chen +5

We present a new method for the verification of quantum circuits based on a novel symbolic representation of sets of quantum states using level-synchronized tree automata (LSTAs).…