Jyun-Ao Lin's Homepage
This site is always under construction….
Personal info
I'm currently an assistant professor in the CSIE and iFIRST of NTUT. Prior joining NTUT, I was a post-doc researcher in K.-M. Chung's Lab at IIS, Academia Sinica. Before switching my interests to computer science, I was a post-doc researcher at IoM, Academia Sinica. I defended my Ph.D. thesis in IMJ-PRG and Universite de Paris-Diderot Paris VII, under the supervission of Prof. Marc Rosso and Prof. Olivier Schiffmann.
- Email: jalin[at]ntut.edu.tw
- Phone: +886-2-2771-2171 #3858
- Office: 宏裕科技大樓 Room 308, NTUT
- Address: No. 1, Sec. 3, Zhongxiao E. Rd., Taipei 10608 Taiwan
Research Interests
quantum program verification, formal method, automata theory, decision procedure of SMT, cryptography, quantum computing and representation theory.
News
I am currently looking for talented and self-motivated students in formal verification, (privacy-preserving) decision procedure and/or verification of quantum programs. If you are interested in working with me, please do not hesitate to contact me via email.
Publications
see DBLP for more details
Recent Journal and Conferences
- P. A. Abdulla, Y.-C. Chen, M. Hečko, L. Holík, L. Lengál, J.-A. Lin, R. T. Srinivasan, Parameterized Verification of Quantum Circuits, POPL 2026, Technical Report.
- Y.-F. Chen, K.-M. Chung, O. Lengál, J.-A. Lin, W.-L. Tsai, Di-De Yen, An Automata-Based Framework for Verification and Bug Hunting in Quantum Circuits, Commun. ACM 68, 6 (June 2025), 85–93. https://doi.org/10.1145/3725728
- Y. F. Chen, K.-M. Chung, M.-H. Hsieh, W.-J. Huang, O. Lengal, J.-A. Lin, W.-L. Tsai, AutoQ 2.0: From Verification of Quantum Circuits to Verification of Quantum Programs, TACAS 2025, Technical Report
- P. A. Abdulla, Y.-C. Chen, Y.-F. Cheng, L. Holik, O. Lengal, J.-A. Lin, F.-Y. Lo, W.-L. Tsai, Verifying Quantum Circuits with Level-Synchronized Tree Automata, POPL 2025, Technical Report,
- Y.-F. Chen, K.-M. Chung, O. Lengal, J.-A. Lin, W.-L. Tsai, AutoQ: An Automata-based Quantum Circuit Verifier, CAV 2023 link
- Y.-F. Chen, K.-M. Chung, O. Lengal, J.-A. Lin, W.-L. Tsai, D.-D. Yen, An Autamata-based Framework for Verification and Bug Hunting in Quantum Circuits, Distinguished Paper Award, PLDI 2023. link, Technical Report
Extended Abstracts
- Jyun-Ao Lin, Yu-Fang Chen, Ondrej Lengal, Fang-Yi Lo, Wei-Lun Tsai, Verifying Repeat-Until-Success Circuits with AutoQ, PLanQC 2026.
- 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, Analysing Quantum Programs using Automata, VQC 2025.
- Y.-F. Chen, K.-M. Chung, O. Lengal, J.-A. Lin, W.-L. Tsai, D.-D. Yen, An Autamata-based Framework for Verification and Bug Hunting in Quantum Circuits, QPL 2023.
Old math publications
- J.-A. Lin, Spherical Hall algebra of a weighted projective curve, International Mathematics Research Notices, https://doi.org/10.1093/imrn/rny158, Vol. 2020, Issue 15, Aug. 2020, 4721–4775.
- J.-A. Lin, A new involution for quantum loop algebras, Journal of Algebra, vol. 480, (2017), 368–384.
Awards
- NSTC 資訊工程學門114年度優良計畫執行成果獎 2025
- SIGLOG/CACM Research Highlights 2025
- Distinguished paper award PLDI 2023
- Post-doc Outstanding Research Award MOST 2018
Teaching
at NTUT
Past
- Theorical Aspects of Modern Cryptograpgy (2021 Spring, 2022 Spring, 2023 Spring NTU CSIE)
- Calculus A (2017-2018 MATH NTU, 2020 Spring XMU Malaysia)
- Advanced Mathematics (2020 Spring, XMU Malaysia)
- Algebra and Analytic Geometry (2019 Fall, XMU Malaysia)
- Engineering Mathematics III (2019 Fall, XMU Malaysia)
- Multi Variables Calculus (2020 Spring, XMU Malaysia)
- Fourier Analysis for physics (2014 Spring, TA Universite de Paris-Sud Orsay)
- WIMS session for Linear Algebras (2014 Spring, TA Universite de Paris-Sud Orsay)
- S1 Mathematics (2013 Fall, TA, Universite de Paris-Sud Orsay)
Tools
- AutoQ: An automata-based C++ tool for quantum program verification.