Publications
2026
- W. Tsai, Y. Chen, and O. Lengal.
A Practical Specification Language for Automatic Quantum Program Verification.
In Proc. of 38th International Conference on Computer Aided Verification — CAV’26,
Lisboa, Portugal,
volume 16684 of LNCS,
pages 302–325, 2026.
Springer-Verlag.
- 📄 preliminary version
- 📝 technical report
- 📊 slides
- 🛠️ AutoQ
- 📦 artifact
- P. A. Abdulla, Y. Chen, M. Hecko, L. Holik, O. Lengal, J. Lin, and R. S. Thinniyam.
Parameterized Verification of Quantum Circuits.
In Proc. of 53rd ACM SIGPLAN Symposium on Principles of Programming Languages — POPL’26, PACMPL 10 (POPL),
Rennes, France,
article 70, pages 2021–2050, 2026.
ACM.
- 📄 preliminary version
- 📊 slides
- 🎥 video
- 🎥 video from a relevant FLAT talk
2025
-
Y. Chen, K. Chung, O. Lengal, J. Lin, W. Tsai, and D. Yen. An Automata-Based Framework for Verification and Bug Hunting in Quantum Circuits. Communications of the ACM (CACM) 68(6), pages 85–93, 2025.
- Y. Chen, K. Chung, M. Hsieh, W. Huang, O. Lengal, J.Lin, and W. Tsai.
AutoQ 2.0: From Verification of Quantum Circuits to Verification of Quantum Programs.
In Proc. of 31th International Conference on Tools and Algorithms for the Construction and Analysis of Systems — TACAS’25,
Hamilton, Canada,
volume 15698 of LNCS,
pages 87–108, 2025.
Springer-Verlag.
- 📄 preliminary version
- 📝 technical report
- 🛠️ AutoQ
- 📦 artifact
- 📊 slides (.pptx)
- P. A. Abdulla, Y. Chen, Y. Chen, L. Holik, O. Lengal, J. Lin, F. Lo, and W. Tsai.
Verifying Quantum Circuits with Level-Synchronized Tree Automata.
In Proc. of 52nd ACM SIGPLAN Symposium on Principles of Programming Languages — POPL’25, PACMPL 9 (POPL),
Denver, Colorado, USA,
article 32, pages 923–953, 2025.
ACM.
- 📄 preliminary version
- 📝 technical report
- 📦 artifact
- 🛠️ AutoQ
- 📊 slides (from VQC’25)
- 🖼️ poster
2024
- T. Chen, Y. Chen, J. Jiang, S. Jobranova, and O. Lengal.
Accelerating Quantum Circuit Simulation with Symbolic Execution and Loop Summarization.
In Proc. of 2024 ACM/IEEE International Conference on Computer-Aided Design — ICCAD’24,
New Jersey, USA,
Article No. 42,
pages 1–9, 2024.
ACM.
- 📄 preliminary version
- 📊 slides
- 🛠️ Medusa
- 📦 artifact
2023
- Y. Chen, K. Chung, O. Lengal, J. Lin, and W. Tsai.
AutoQ: An Automata-based Quantum Circuit Verifier.
In Proc. of 35th International Conference on Computer Aided Verification — CAV’23,
Paris, France,
volume 13966 of LNCS,
pages 139–153, 2023.
Springer-Verlag.
- 📄 preliminary version
- 📦 artifact
- 🛠️ AutoQ
- Y. Chen, K. Chung, O. Lengal, J. Lin, W. Tsai, and D. Yen.
An Automata-based Framework for Verification and Bug Hunting in Quantum Circuits.
In Proc. of 44th ACM SIGPLAN Conference on Programming Language Design and Implementation — PLDI’23, PACMPL 7 (PLDI),
Orlando, Florida, USA,
article 156, pages 1218–1243, 2023.
ACM.
- 📄 preliminary version
- 📝 technical report
- 📦 artifact
- 🎥 video
- 📊 slides (.pptx)
- 🛠️ AutoQ
- 🏆 Distinguished Paper of PLDI’23