GOAL: A Graphical Tool for Manipulating Büchi Automata and Temporal Formulae. - Yih-Kuen Tsay; Yu-Fang Chen 001; Ming-Hsien Tsai 001; Kang-Nien Wu; Wen-Chin Chan (TACAS, 2007)

Extending Automated Compositional Verification to the Full Class of Omega-Regular Languages. - Azadeh Farzan; Yu-Fang Chen 001; Edmund M. Clarke; Yih-Kuen Tsay; Bow-Yaw Wang (TACAS, 2008)

GOAL Extended: Towards a Research Tool for Omega Automata and Temporal Logic. - Yih-Kuen Tsay; Yu-Fang Chen 001; Ming-Hsien Tsai 001; Wen-Chin Chan; Chi-Jian Luo (TACAS, 2008)

Learning Minimal Separating DFA's for Compositional Verification. - Yu-Fang Chen 001; Azadeh Farzan; Edmund M. Clarke; Yih-Kuen Tsay; Bow-Yaw Wang (TACAS, 2009)

Tool support for learning Büchi automata and linear temporal logic. - Yih-Kuen Tsay; Yu-Fang Chen 001; Ming-Hsien Tsai 001; Kang-Nien Wu; Wen-Chin Chan; Chi-Jian Luo; Jinn-Shu Chang (Formal Aspects Comput., 2009)

Simulation Subsumption in Ramsey-Based Büchi Automata Universality and Inclusion Testing. - Parosh Aziz Abdulla; Yu-Fang Chen 001; Lorenzo Clemente; Lukás Holík; Chih-Duo Hong; Richard Mayr; Tomás Vojnar (CAV, 2010)

Automated Assume-Guarantee Reasoning through Implicit Learning. - Yu-Fang Chen 001; Edmund M. Clarke; Azadeh Farzan; Ming-Hsien Tsai 001; Yih-Kuen Tsay; Bow-Yaw Wang (CAV, 2010)

Constrained Monotonic Abstraction: A CEGAR for Parameterized Verification. - Parosh Aziz Abdulla; Yu-Fang Chen 001; Giorgio Delzanno; Frédéric Haziza; Chih-Duo Hong; Ahmed Rezine (CONCUR, 2010)

Comparing Learning Algorithms in Automated Assume-Guarantee Reasoning. - Yu-Fang Chen 001; Edmund M. Clarke; Azadeh Farzan; Fei He 001; Ming-Hsien Tsai 001; Yih-Kuen Tsay; Bow-Yaw Wang; Lei Zhu (ISoLA (1), 2010)

When Simulation Meets Antichains. - Parosh Aziz Abdulla; Yu-Fang Chen 001; Lukás Holík; Richard Mayr; Tomás Vojnar (TACAS, 2010)

Algorithms for Synthesizing Priorities in Component-Based Systems. - Chih-Hong Cheng; Saddek Bensalem; Yu-Fang Chen 001; Rongjie Yan; Barbara Jobstmann; Harald Ruess; Christian Buckl; Alois C. Knoll (ATVA, 2011)

Advanced Ramsey-Based Büchi Automata Inclusion Testing. - Parosh Aziz Abdulla; Yu-Fang Chen 001; Lorenzo Clemente; Lukás Holík; Chih-Duo Hong; Richard Mayr; Tomás Vojnar (CONCUR, 2011)

Learning Boolean Functions Incrementally. - Yu-Fang Chen 001; Bow-Yaw Wang (CAV, 2012)

Automatic Fence Insertion in Integer Programs via Predicate Abstraction. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Yu-Fang Chen 001; Carl Leonardsson; Ahmed Rezine (SAS, 2012)

Counter-Example Guided Fence Insertion under TSO. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Yu-Fang Chen 001; Carl Leonardsson; Ahmed Rezine (TACAS, 2012)

Memorax, a Precise and Sound Tool for Automatic Fence Insertion under TSO. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Yu-Fang Chen 001; Carl Leonardsson; Ahmed Rezine (TACAS, 2013)

BULL: A Library for Learning Algorithms of Boolean Functions. - Yu-Fang Chen 001; Bow-Yaw Wang (TACAS, 2013)

A Finite Exact Representation of Register Automata Configurations. - Yu-Fang Chen 001; Bow-Yaw Wang; Di-De Yen (INFINITY, 2013)

Learning Summaries of Recursive Functions. - Yu-Fang Chen 001; Bow-Yaw Wang; Kai-Chun Yang (APSEC (1), 2014)

String Constraints for Verification. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Yu-Fang Chen 001; Lukás Holík; Ahmed Rezine; Philipp Rümmer; Jari Stenman (CAV, 2014)

Verifying Curve25519 Software. - Yu-Fang Chen 001; Chang-Hong Hsu; Hsin-Hung Lin; Peter Schwabe; Ming-Hsien Tsai 001; Bow-Yaw Wang; Bo-Yin Yang; Shang-Yi Yang (CCS, 2014)

Verifying Recursive Programs Using Intraprocedural Analyzers. - Yu-Fang Chen 001; Chiao Hsieh; Ming-Hsien Tsai 001; Bow-Yaw Wang; Farn Wang (SAS, 2014)

Mediating for reduction (on minimizing alternating Büchi automata). - Parosh Aziz Abdulla; Yu-Fang Chen 001; Lukás Holík; Tomás Vojnar (Theor. Comput. Sci., 2014)

Norn: An SMT Solver for String Constraints. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Yu-Fang Chen 001; Lukás Holík; Ahmed Rezine; Philipp Rümmer; Jari Stenman (CAV (1), 2015)

Counterexample-Guided Polynomial Loop Invariant Generation by Lagrange Interpolation. - Yu-Fang Chen 001; Chih-Duo Hong; Bow-Yaw Wang; Lijun Zhang 001 (CAV (1), 2015)

Commutativity of Reducers. - Yu-Fang Chen 001; Chih-Duo Hong; Nishant Sinha 001; Bow-Yaw Wang (TACAS, 2015)

CPArec: Verifying Recursive Programs via Source-to-Source Program Transformation - (Competition Contribution). - Yu-Fang Chen 001; Chiao Hsieh; Ming-Hsien Tsai 001; Bow-Yaw Wang; Farn Wang (TACAS, 2015)

The Commutativity Problem of the MapReduce Framework: A Transducer-Based Approach. - Yu-Fang Chen 001; Lei Song; Zhilin Wu (CAV (2), 2016)

PAC learning-based verification and model synthesis. - Yu-Fang Chen 001; Chiao Hsieh; Ondrej Lengál; Tsung-Ju Lii; Ming-Hsien Tsai 001; Bow-Yaw Wang; Farn Wang (ICSE, 2016)

Optimal sanitization synthesis for web application vulnerability repair. - Fang Yu 001; Ching-Yuan Shueh; Chun-Han Lin; Yu-Fang Chen 001; Bow-Yaw Wang; Tevfik Bultan (ISSTA, 2016)

Learning to prove safety over parameterised concurrent systems. - Yu-Fang Chen 001; Chih-Duo Hong; Anthony W. Lin; Philipp Rümmer (FMCAD, 2017)

Register automata with linear arithmetic. - Yu-Fang Chen 001; Ondrej Lengál; Tony Tan; Zhilin Wu (LICS, 2017)

An Executable Sequential Specification for Spark Aggregation. - Yu-Fang Chen 001; Chih-Duo Hong; Ondrej Lengál; Shin-Cheng Mu; Nishant Sinha 001; Bow-Yaw Wang (NETYS, 2017)

Flatten and conquer: a framework for efficient analysis of string constraints. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Yu-Fang Chen 001; Bui Phi Diep; Lukás Holík; Ahmed Rezine; Philipp Rümmer (PLDI, 2017)

Learning to Prove Safety over Parameterised Concurrent Systems (Full Version). - Yu-Fang Chen 001; Chih-Duo Hong; Anthony W. Lin; Philipp Rümmer (CoRR, 2017)

Trau: SMT solver for string constraints. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Yu-Fang Chen 001; Bui Phi Diep; Lukás Holík; Ahmed Rezine; Philipp Rümmer (FMCAD, 2018)

Advanced automata-based algorithms for program termination checking. - Yu-Fang Chen 001; Matthias Heizmann; Ondrej Lengál; Yong Li 031; Ming-Hsien Tsai 001; Andrea Turrini; Lijun Zhang 001 (PLDI, 2018)

Learning Büchi Automata and Its Applications. - Yong Li 031; Andrea Turrini; Yu-Fang Chen 001; Lijun Zhang 001 (SETSS, 2018)

Ultimate Automizer and the Search for Perfect Interpolants - (Competition Contribution). - Matthias Heizmann; Yu-Fang Chen 001; Daniel Dietsch; Marius Greitschus; Jochen Hoenicke; Yong Li 031; Alexander Nutz; Betim Musa; Christian Schilling 001; Tanja Schindler; Andreas Podelski (TACAS (2), 2018)

J-ReCoVer: Java Reducer Commutativity Verifier. - Yu-Fang Chen 001; Chang-Yi Chiang; Lukás Holík; Wei-Tsung Kao; Hsin-Hung Lin; Tomás Vojnar; Yean-Fu Wen; Wei-Cheng Wu (APLAS, 2019)

Simulations in Rank-Based Büchi Automata Complementation. - Yu-Fang Chen 001; Vojtech Havlena; Ondrej Lengál (APLAS, 2019)

Synthesize Models for Quantitative Analysis Using Automata Learning. - Yu-Fang Chen 001; Hsiao-chen Chung; Wen-Chi Hung; Ming-Hsien Tsai 001; Bow-Yaw Wang; Farn Wang (NETYS, 2019)

ROLL 1.0: omega -Regular Language Learning Library. - Yong Li 031; Xuechao Sun; Andrea Turrini; Yu-Fang Chen 001; Junnan Xu (TACAS (1), 2019)

A Symbolic Algorithm for the Case-Split Rule in String Constraint Solving. - Yu-Fang Chen 001; Vojtech Havlena; Ondrej Lengál; Andrea Turrini (APLAS, 2020)

Determinizing Crash Behavior with a Verified Snapshot-Consistent Flash Translation Layer. - Yun-Sheng Chang; Yao Hsiao; Tzu-Chi Lin; Che-Wei Tsao; Chun-Feng Wu; Yuan-Hao Chang 001; Hsiang-Shang Ko; Yu-Fang Chen 001 (OSDI, 2020)

Efficient handling of string-number conversion. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Yu-Fang Chen 001; Bui Phi Diep; Julian Dolby; Petr Janku; Hsin-Hung Lin; Lukás Holík; Wei-Cheng Wu (PLDI, 2020)

Performance enhancement for iterative data computing with in-memory concurrent processing. - Yean-Fu Wen; Yu-Fang Chen 001; Tse Kai Chiu; Yen-Chou Chen (Concurr. Comput. Pract. Exp., 2020)

Solving Not-Substring Constraint withFlat Abstraction. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Yu-Fang Chen 001; Bui Phi Diep; Lukás Holík; Denghang Hu; Wei-Lun Tsai; Zhilin Wu; Di-De Yen (APLAS, 2021)

PyCT: A Python Concolic Tester. - Yu-Fang Chen 001; Wei-Lun Tsai; Wei-Cheng Wu; Di-De Yen; Fang Yu 001 (APLAS, 2021)

Weakly Durable High-Performance Transactions. - Yun-Sheng Chang; Yu-Fang Chen 001; Hsiang-Shang Ko (CoRR, 2021)

A novel learning algorithm for Büchi automata based on family of DFAs and classification trees. - Yong Li 031; Yu-Fang Chen 001; Lijun Zhang 001; Depeng Liu (Inf. Comput., 2021)

Optimization-Based Resource Management Algorithms with Considerations of Client Satisfaction and High Availability in Elastic 5G Network Slices. - Chiu-Han Hsiao; Frank Yeong-Sung Lin; Evana Szu-Han Fang; Yu-Fang Chen 001; Yean-Fu Wen; Yennun Huang; Yang-Che Su; Ya-Syuan Wu; Hsin-Yi Kuo (Sensors, 2021)

Optimization-Based Approaches for Minimizing Deployment Costs for Wireless Sensor Networks with Bounded Estimation Errors. - Chiu-Han Hsiao; Frank Yeong-Sung Lin; Hao-Jyun Yang; Yennun Huang; Yu-Fang Chen 001; Ching-Wen Tu; Si-Yao Zhang (Sensors, 2021)

Word Equations in Synergy with Regular Constraints (Technical Report). - Frantisek Blahoudek; Yu-Fang Chen 001; David Chocholatý; Vojtech Havlena; Lukás Holík; Ondrej Lengál; Juraj Síc (CoRR, 2022)

An Optimization-Based Orchestrator for Resource Access and Operation Management in Sliced 5G Core Networks. - Chiu-Han Hsiao; Yean-Fu Wen; Frank Yeong-Sung Lin; Yu-Fang Chen 001; Yennun Huang; Yang-Che Su; Ya-Syuan Wu (Sensors, 2022)

A Theory of Cartesian Arrays (with Applications in Quantum Circuit Verification). - Yu-Fang Chen 001; Philipp Rümmer; Wei-Lun Tsai (CADE, 2023)

AutoQ: An Automata-Based Quantum Circuit Verifier. - Yu-Fang Chen 001; Kai-Min Chung; Ondrej Lengál; Jyun-Ao Lin; Wei-Lun Tsai (CAV (3), 2023)

Word Equations in Synergy with Regular Constraints. - Frantisek Blahoudek; Yu-Fang Chen 001; David Chocholatý; Vojtech Havlena; Lukás Holík; Ondrej Lengál; Juraj Síc (FM, 2023)

FSD: File-related Secure Deletion to Prolong the Lifetime of Solid-State Drives. - Shih-Chun Chou; Yi-Shen Chen; Ping-Xiang Chen; Yuan-Hao Chang 001; Ming-Chang Yang; Tei-Wei Kuo; Yu-Fang Chen 001; Yu-Ming Chang (NVMSA, 2023)

An Automata-based Framework for Verification and Bug Hunting in Quantum Circuits (Technical Report). - Yu-Fang Chen 001; Kai-Min Chung; Ondrej Lengál; Jyun-Ao Lin; Wei-Lun Tsai; Di-De Yen (CoRR, 2023)

A Symbolic Algorithm for the Case-Split Rule in Solving Word Constraints with Extensions (Technical Report). - Yu-Fang Chen 001; Vojtech Havlena; Ondrej Lengál; Andrea Turrini (CoRR, 2023)

Z3-Noodler: An Automata-based String Solver (Technical Report). - Yu-Fang Chen 001; David Chocholatý; Vojtech Havlena; Lukás Holík; Ondrej Lengál; Juraj Síc (CoRR, 2023)

A symbolic algorithm for the case-split rule in solving word constraints with extensions. - Yu-Fang Chen 001; Vojtech Havlena; Ondrej Lengál; Andrea Turrini (J. Syst. Softw., 2023)

Solving String Constraints with Lengths by Stabilization. - Yu-Fang Chen 001; David Chocholatý; Vojtech Havlena; Lukás Holík; Ondrej Lengál; Juraj Síc (Proc. ACM Program. Lang., 2023)

Accelerating Quantum Circuit Simulation with Symbolic Execution and Loop Summarization. - Tian-Fu Chen; Yu-Fang Chen 001; Jie-Hong Roland Jiang; Sára Jobranová; Ondrej Lengál (ICCAD, 2024)

Z3-Noodler: An Automata-based String Solver. - Yu-Fang Chen 001; David Chocholatý; Vojtech Havlena; Lukás Holík; Ondrej Lengál; Juraj Síc (TACAS (1), 2024)

Constraint-based Adversarial Example Synthesis. - Fang Yu; Ya-Yu Chi; Yu-Fang Chen 001 (CoRR, 2024)

Verifying Quantum Circuits with Level-Synchronized Tree Automata (Technical Report). - Parosh Aziz Abdulla; Yo-Ga Chen; Yu-Fang Chen 001; Lukás Holík; Ondrej Lengál; Jyun-Ao Lin; Fang-Yi Lo; Wei-Lun Tsai (CoRR, 2024)

A decision procedure for string constraints with string/integer conversion and flat regular constraints. - Hao Wu 085; Yu-Fang Chen 001; Zhilin Wu; Bican Xia; Naijun Zhan (Acta Informatica, 2024)

AutoQ 2.0: From Verification of Quantum Circuits to Verification of Quantum Programs. - Yu-Fang Chen 001; Kai-Min Chung; Min-Hsiu Hsieh; Wei-Jia Huang; Ondrej Lengál; Jyun-Ao Lin; Wei-Lun Tsai (TACAS (3), 2025)

Verifying Quantum Circuits with Level-Synchronized Tree Automata. - Parosh Aziz Abdulla; Yo-Ga Chen; Yu-Fang Chen 001; Lukás Holík; Ondrej Lengál; Jyun-Ao Lin; Fang-Yi Lo; Wei-Lun Tsai (Proc. ACM Program. Lang., 2025)

A Uniform Framework for Handling Position Constraints in String Solving. - Yu-Fang Chen 001; Vojtech Havlena; Michal Hecko; Lukás Holík; Ondrej Lengál (Proc. ACM Program. Lang., 2025)

A Uniform Framework for Handling Position Constraints in String Solving (Technical Report). - Yu-Fang Chen 001; Vojtech Havlena; Michal Hecko; Lukás Holík; Ondrej Lengál (CoRR, 2025)

An Automata-Based Framework for Verification and Bug Hunting in Quantum Circuits. - Yu-Fang Chen 001; Kai-Min Chung; Ondrej Lengál; Jyun-Ao Lin; Wei-Lun Tsai; Di-De Yen (Commun. ACM, 2025)

Adaptive Traffic Control: OpenFlow-Based Prioritization Strategies for Achieving High Quality of Service in Software-Defined Networking. - Yu-Fang Chen 001; Frank Yeong-Sung Lin; Sheng-Yung Hsu; Tzu-Lung Sun; Yennun Huang; Chiu-Han Hsiao (IEEE Trans. Netw. Serv. Manag., 2025)

A near-optimal resource allocation strategy for minimizing the worse-case impact of malicious attacks on cloud networks. - Yu-Fang Chen 001; Frank Yeong-Sung Lin; Kuang-Yen Tai; Chiu-Han Hsiao; Wei-Hsin Wang; Ming-Chi Tsai; Tzu-Lung Sun (J. Cloud Comput., 2025)