=====Publications ===== 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 [{{{{ :pldi2020.pdf |preprint}}] \\ **PLDI 2020** Yu-Fang Chen, Vojtech Havlena, Ondrej Lengál\\ Simulations in Rank-Based Büchi Automata Complementation. [{{{{ :simulation.pdf |preprint}}]\\ **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. [{{{{ :jrecover.pdf |preprint}}]\\ **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. [{{{{ :learnMA.pdf |preprint}}]\\ **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** Yu-Fang Chen, Chih-Duo Hong, Anthony W. Lin, Phillipp Rümmer\\ Learning to Prove Safety over Parameterised Concurrent Systems [{{ ::fmcad17_full.pdf |preprint}}]\\ **FMCAD 2017** Yu-Fang Chen, Ondrej Lengál, Tony Tan, Zhilin Wu\\ Register Automata with Linear Arithmetic [{{ :131.pdf |preprint}}]\\ **LICS 2017** Parosh Aziz Abdulla, Mohamed Faouzi Atig, Phi-Diep Bui, Yu-Fang Chen, Lukáš Holík, Ahmed Rezine, Philipp Rümmer\\ Flatten and Conquer (A Framework for Efficient Analysis of String Constraints) [{{ :pldi2017.pdf |preprint}}]\\ **PLDI 2017** Yong Li, Yu-Fang Chen, Lijun Zhang and Depeng Liu\\ A Novel Learning Algorithm for Buchi Automata based on Family of DFAs and Classification Trees [{{:tacas_2017.pdf |preprint}}]\\ **TACAS 2017** Yu-Fang Chen, Chih-Duo Hong, Ondrej Lengál, Shin-Cheng Mu, Nishant Sinha, Bow-Yaw Wang\\ An Executable Sequential Specification for Spark Aggregation [{{ ::netys2017.pdf |preprint}}]\\ **NETYS 2017** Yu-Fang Chen, Lei Song, Zhilin Wu\\ The Commutativity Problem of the MapReduce Framework: A Transducer-Based Approach [{{ :cav2016.pdf |preprint}}]\\ **CAV 2016** Yu-Fang Chen, Chiao Hsieh, Ondrej Lengál, Tsung-Ju Lii, Ming-Hsien Tsai, Bow-Yaw Wang, Farn Wang\\ PAC Learning-based Verification and Model Synthesis [{{ :icse2016.pdf |preprint}}]\\ **ICSE 2016** Fang Yu, Ching-Yuan Shueh, Chun-Han Lin, Yu-Fang Chen, Bow-Yaw Wang, Tevfik Bultan\\ Optimal Sanitization Synthesis for Web Application Vulnerability Repair [{{ :issta2016.pdf |preprint}}]\\ **ISSTA 2016** Parosh A. Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Lukás Holík, Ahmed Rezine, Philipp Rümmer, Jari Stenman\\ Norn: An SMT Solver for String Constraints [{{ :cav2015_norn.pdf |preprint}}]\\ **CAV 2015** Yu-Fang Chen, Chih-Duo Hong, Bow-Yaw Wang, Lijun Zhang\\ Counterexample-Guided Polynomial Loop Invariant Generation by Lagrange Interpolation [{{ :cav2015_lagrange.pdf |preprint}}]\\ **CAV 2015** Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, Bow-Yaw Wang\\ Commutativity of Reducers [{{ :tacas2015_reducers.pdf |preprint}}]\\ **TACAS 2015** Yu-Fang Chen, Chiao Hsieh, Ming-Hsien Tsai, Bow-Yaw Wang, Farn Wang\\ CPArec: Verifying Recursive Programs via Source-to-Source Program Transformation (SVCOMP) [{{ :sv-comp2015.pdf |preprint}}]\\ **TACAS 2015** Parosh Aziz Abdulla, Yu-Fang Chen, Lukás Holík, Tomás Vojnar\\ Mediating for reduction (on minimizing alternating Büchi automata)\\ **Theoretical Computer Science 2014** Yu-Fang Chen, Bow-Yaw Wang, Kai-Chun Yang\\ Learning Summaries of Recursive Functions [{{ :apsec14.pdf |preprint}}]\\ **APSEC 2014** Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Lukás Holík, Ahmed Rezine, Philipp Rümmer, Jari Stenman\\ String Constraints for Verification [{{ ::cav2014-1.pdf |preprint}}]\\ **CAV 2014** Yu-Fang Chen, Chang-Hong Hsu, Hsin-Hung Lin, Peter Schwabe, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang, Shang-Yi Yang\\ Verifying Curve25519 Software [{{ :ccs2014.pdf |preprint}}]\\ **CCS 2014** Yu-Fang Chen, Chiao Hsieh, Ming-Hsien Tsai, Bow-Yaw Wang, Farn Wang\\ Verifying Recursive Programs Using Intraprocedural Analyzers [{{ :sas2014.pdf |preprint}}]\\ **SAS 2014** Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Carl Leonardsson, Ahmed Rezine\\ Memorax, a Precise and Sound Tool for Automatic Fence Insertion under TSO [{{ :tacas_2013.pdf |preprint}}]\\ **TACAS 2013** Yu-Fang Chen, Bow-Yaw Wang\\ BULL: A Library for Learning Algorithms of Boolean Functions [{{ :tacas2013.pdf |[preprint}}]\\ **TACAS 2013** Yu-Fang Chen, Bow-Yaw Wang, Di-De Yen\\ A Finite Exact Representation of Register Automata Configurations\\ **INFINITY 2013** Yu-Fang Chen, Bow-Yaw Wang\\ Learning Boolean Functions Incrementally [{{ :cav2012.pdf |preprint}}]\\ **CAV 2012** Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Carl Leonardsson, Ahmed Rezine\\ Automatic Fence Insertion in Integer Programs via Predicate Abstraction [{{ :sas_2012.pdf |preprint}}]\\ **SAS 2012** Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Carl Leonardsson, Ahmed Rezine\\ Counter-Example Guided Fence Insertion under TSO [{{ :tacas_2012.pdf |preprint}}]\\ **TACAS 2012** Chih-Hong Cheng, Saddek Bensalem, Yu-Fang Chen, Rongjie Yan, Barbara Jobstmann, Harald Ruess, Christian Buckl, Alois Knoll\\ Algorithms for Synthesizing Priorities in Component-Based Systems\\ **ATVA 2011** Parosh Aziz Abdulla, Yu-Fang Chen, Lorenzo Clemente, Lukás Holík, Chih-Duo Hong, Richard Mayr, Tomás Vojnar\\ Advanced Ramsey-Based Büchi Automata Inclusion Testing [{{ :concur2011.pdf |preprint}}]\\ **CONCUR 2011** Parosh Aziz Abdulla, Yu-Fang Chen, Lorenzo Clemente, Lukás Holík, Chih-Duo Hong, Richard Mayr, Tomás Vojnar\\ Simulation Subsumption in Ramsey-Based Büchi Automata Universality and Inclusion Testing [{{ :cav_2010.pdf |preprint}}]\\ **CAV 2010** Yu-Fang Chen, Edmund M. Clarke, Azadeh Farzan, Ming-Hsien Tsai, Yih-Kuen Tsay, Bow-Yaw Wang\\ Automated Assume-Guarantee Reasoning through Implicit Learning [{{ :cav10-learning.pdf |preprint}}]\\ **CAV 2010** Parosh Aziz Abdulla, Yu-Fang Chen, Giorgio Delzanno, Frédéric Haziza, Chih-Duo Hong, Ahmed Rezine\\ Constrained Monotonic Abstraction: A CEGAR for Parameterized Verification [{{ :concur2010.pdf |preprint}}]\\ **CONCUR 2010** Yu-Fang Chen, Edmund M. Clarke, Azadeh Farzan, Fei He, Ming-Hsien Tsai, Yih-Kuen Tsay, Bow-Yaw Wang, Lei Zhu\\ Comparing Learning Algorithms in Automated Assume-Guarantee Reasoning [{{ :isola2010.pdf |preprint}}]\\ **ISoLA 2010** Parosh Aziz Abdulla, Yu-Fang Chen, Lukás Holík, Richard Mayr, Tomás Vojnar\\ When Simulation Meets Antichains [{{ :tacas_2010.pdf |preprint}}]\\ **TACAS 2010** (Best Paper Award) Yih-Kuen Tsay, Yu-Fang Chen, Ming-Hsien Tsai, Kang-Nien Wu, Wen-Chin Chan, Chi-Jian Luo, Jinn-Shu Chang\\ Tool support for learning Büchi automata and linear temporal logic\\ **Formal Aspect of Computing 2009** Parosh Aziz Abdulla, Yu-Fang Chen, Lukás Holík, Tomás Vojnar\\ Mediating for Reduction (on Minimizing Alternating Büchi Automata) [{{ :fsttcs2009.pdf |preprint}}]\\ **FSTTCS 2009** Yu-Fang Chen, Azadeh Farzan, Edmund M. Clarke, Yih-Kuen Tsay, Bow-Yaw Wang\\ Learning Minimal Separating DFA's for Compositional Verification [{{ :tacas_2009.pdf |preprint}}]\\ **TACAS 2009** Azadeh Farzan, Yu-Fang Chen, Edmund M. Clarke, Yih-Kuen Tsay, Bow-Yaw Wang\\ Extending Automated Compositional Verification to the Full Class of Omega-Regular Languages [{{ :tacas_2008.pdf |preprint}}]\\ **TACAS 2008** Yih-Kuen Tsay, Yu-Fang Chen, Ming-Hsien Tsai, Wen-Chin Chan, Chi-Jian Luo\\ GOAL Extended: Towards a Research Tool for Omega Automata and Temporal Logic\\ **TACAS 2008** Yih-Kuen Tsay, Yu-Fang Chen, Ming-Hsien Tsai, Kang-Nien Wu, Wen-Chin Chan\\ GOAL: A Graphical Tool for Manipulating Büchi Automata and Temporal Formulae\\ **TACAS 2007**