{{ :34289781435_d833a98007_m.jpg|}} ===== Information===== *Yu-Fang Chen {{:name.png?50|}} * Research Fellow (equivalent to the full professor rank in universities), Institute of Information Science, Academia Sinica *Email: yfc@iis.sinica.edu.tw *Phone: +886-2-2788-3799 #1514 *Address: No.128, Section 2, Academia Road, Nankang District, Taipei 115, Taiwan ==== Awards ==== * Distinguished paper award **OOPSLA 2023** * Young Scholar Creativity Award, Foundation for Advancement of Outstanding Scholarship, Taiwan, 2023 * Distinguished paper award **PLDI 2023** * Best paper award **FM 2023** * MOST Research Project for Excellent Junior Research Investigators 2020-2023. * Best paper award **TACAS 2010** ==== Research interests ==== * Formal Verification * Automata theory * Satisfibility Modulo Theory * Quantum Algortihms =====Recent Publications ===== Hao Wu, Yu-Fang Chen, Zhilin Wu, Bican Xia, Naijun Zhan\\ A Decision Procedure for String Constraints with String/Integer Conversion and Flat Regular Constraints.\\ **Acta Informatica 2024**\\ Yu-Fang Chen, David Chocholatý, Vojtech Havlena, Lukás Holík, Ondrej Lengál, Juraj Síc\\ Z3-Noodler: An Automata-based String Solver.\\ **TACAS 2024 (Best paper nomination)**\\ Yu-Fang Chen, Vojtech Havlena, Ondrej Lengál, Andrea Turrini\\ A symbolic Algorithm for the Case-split Rule in Solving Word Constraints with Extensions.\\ **Journal System Software 2023**\\ Yu-Fang Chen, David Chocholaty, Vojtech Havlena, Lukás Holik, Ondrej Lengal, Juraj Síc\\ Solving String Constraints with Lengths by Stabilization.\\ **OOPSLA 2023 (Distinguished paper award)** Yu-Fang Chen, Philipp Rümmer and Wei-Lun Tsai\\ A Theory of Cartesian Arrays with Applications in Quantum Circuit Verification.\\ **CADE 2023**\\ Yu-Fang Chen, Kai-Min Chung, Ondřej Lengál, Jyun-Ao Lin, Wei-Lun Tsai.\\ AutoQ: An Automata-based Quantum Circuit Verifier. [[https://link.springer.com/chapter/10.1007/978-3-031-37709-9_7|Link]]\\ **CAV 2023**\\ Yu-Fang Chen, Kai-Min Chung, Ondřej Lengál, Jyun-Ao Lin, Wei-Lun Tsai, Di-De Yen.\\ An Automata-based Framework for Verification and Bug Hunting in Quantum Circuits [[https://doi.org/10.1145/3591270|Link]][[https://www.youtube.com/live/1L1eKWwa6fE?t=4481|Talk at PLDI2023]]{{ :313.pptx |Slides}}\\ **PLDI 2023 (Distinguished paper award)** and a presentation at **QPL 2023**\\ Frantisek Blahoudek, Yu-Fang Chen, David Chocholaty, Vojtech Havlena, Lukás Holik, Ondrej Lengal, Juraj Síc.\\ Word Equations in Synergy with Regular Constraints. [[https://link.springer.com/chapter/10.1007/978-3-031-27481-7_23|Link]]\\ **FM 2023 (Best paper award)** Yong Li, Yu-Fang Chen, Lijun Zhang,Depeng Liu\\ A novel learning algorithm for Büchi automata based on family of DFAs and classification trees [[https://www.sciencedirect.com/science/article/pii/S0890540120301711?via%3Dihub|Link]]\\ **Information and Computation 2021** Yu-Fang Chen, Wei-Lun Tsai, Wei-Cheng Wu, Di-De Yen, Fang Yu\\ PyCT: A Python Concolic Tester. [[https://link.springer.com/chapter/10.1007/978-3-030-89051-3_3|Link]]\\ **APLAS 2021** Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Bui Phi Diep, Lukás Holík, Denghang Hu, Wei-Lun Tsai, Zhilin Wu, Di-De Yen\\ Solving Not-Substring Constraint with Flat Abstraction. [[https://link.springer.com/chapter/10.1007/978-3-030-89051-3_17|Link]]\\ **APLAS 2021** Yu-Fang Chen, Vojtech Havlena, Ondrej Lengal, and Andrea Turrini\\ A Symbolic Algorithm for the Case-Split Rule in String Constraint Solving [[https://link.springer.com/chapter/10.1007/978-3-030-64437-6_18|Link]]\\ **APLAS 2020** Yun-Sheng Chang, Yao Hsiao, Tzu-Chi Lin, Che-Wei Tsao, Chun-Feng Wu, Yuan-Hao Chang, Hsiang-Shang Ko, and Yu-Fang Chen\\ Determinizing Crash Behavior with a Verified Snapshot-Consistent Flash Translation Layer [[https://www.usenix.org/conference/osdi20/presentation/chang|Link]]\\ **OSDI 2020** Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Phi-Diep Bui, Julian Dolby, Petr Janku, Hsin-Hung Lin, Lukas Holik, Wei-Cheng Wu\\ Efficient Handling of String-Number Conversion [[https://dx.doi.org/10.1145/3385412.3386034|Link]]\\ **PLDI 2020** Yu-Fang Chen, Vojtech Havlena, Ondrej Lengál\\ Simulations in Rank-Based Büchi Automata Complementation. [[https://link.springer.com/chapter/10.1007/978-3-030-34175-6_23|Link]]\\ **APLAS 2019** Yu-Fang Chen, Chang-Yi Chiang, Lukás Holík, Wei-Tsung Kao, Hsin-Hung Lin, Tomás Vojnar, Yean-Fu Wen, Wei-Cheng Wu\\ J-ReCoVer: Java Reducer Commutativity Verifier. [[https://link.springer.com/chapter/10.1007/978-3-030-34175-6_18|Link]]\\ **APLAS 2019** Yu-Fang Chen, Hsiao-chen Chung, Wen-Chi Hung, Ming-Hsien Tsai, Bow-Yaw Wang, Farn Wang\\ Synthesize Models for Quantitative Analysis Using Automata Learning. [[https://link.springer.com/chapter/10.1007/978-3-030-31277-0_6|Link]]\\ **NETYS 2019** Yong Li, Xuechao Sun, Andrea Turrini, Yu-Fang Chen, Junnan Xu\\ ROLL 1.0: Omega-Regular Language Learning Library [{{{{ :roll.pdf |preprint}}]\\ **TACAS 2019** Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Bui Phi Diep, Lukás Holík, Ahmed Rezine, Philipp Rümmer\\ Trau: SMT solver for string constraints [{{ ::fmcad2018.pdf |preprint}}]\\ **FMCAD 2018** Yu-Fang Chen, Matthias Heizmann, Ondrej Lengal, Yong Li, Ming-Hsien Tsai, Andrea Turrini, Lijun Zhang\\ Advanced Automata-based Algorithms for Program Termination Checking [{{ ::pldi2018.pdf |preprint}}]\\ **PLDI 2018** Matthias Heizmann, Yu-Fang Chen, Daniel Dietsch, Marius Greitschus, Jochen Hoenicke, Yong Li, Alexander Nutz, Betim Musa, Christian Schilling, Tanja Schindler, and Andreas Podelski\\ Ultimate Automizer and the Search for Perfect Interpolants (Competition Contribution) [{{ ::tacas2018.pdf |preprint}}]\\ **TACAS 2018** [[publications|Earlier Publications]] =====Services===== ====Recent PC Duties==== **2025** FoSSaCS\\ **2024** CAV, ATVA, CONCUR, DATE, NETYS\\ **2023** CAV, ATVA, SAS, DATE\\ **2022** CAV, ATVA, VMCAI\\ **2021** LICS, ATVA, FASE, VMCAI\\ **2020** CONCUR, ATVA, FASE\\ **2019** TACAS, ATVA, SAS ====Steering Committee==== ATVA ====Organizers==== MOSCA 2023@CAV\\ Flolac Summer School 2023\\ ATVA 2019 ===== Projects ===== * [[http://www.languageinclusion.org|Languageinclusion.org--A collection of recent research results on automata language inclusion testing]] * [[http://bull.iis.sinica.edu.tw|Boolean fUnction Learning Library (BULL)]] *[[http://goal.im.ntu.edu.tw|The GOAL Tool]] *[[http://iscasmc.ios.ac.cn/roll|Regular Omega Language Learning (ROLL) Library]] *[[https://github.com/fmlab-iis/ma-learning/wiki|Multiplicity Automata Learning Library (MALL)]] *[[http://user.it.uu.se/~jarst116/norn/|Norn, a solver for string constraints]]