Page 174 - My FlipBook
P. 174
研
人 Research Fellow
員 陳郁方 Yu-Fang Chen
Faculty Ph.D., Information Management, National Taiwan University, Taiwan
T +886-2-2788-3799 ext. 1514 E yfc@iis.sinica.edu.tw
F +886-2-2782-4814 W www.iis.sinica.edu.tw/pages/yfc
・ Research Fellow, IIS, Academia Sinica (2018-present)
・ Professor, IM, National Taiwan University (2019)
・ Professor, MIS, National Taipei University (2019-present)
・ Associate Research Fellow, IIS, Academia Sinica (2014-2018)
・ Adjunct Associate Professor, MIS, National Taipei University (2014-2019)
・ Adjunct Assistant Professor, IM, National Taiwan University (2010-2014)
・ Assistant Research Fellow, IIS, Academia Sinica (2009-2014)
・ PostDoc, Uppsala University (2009)
・ EATCS (European Association for Theoretical Computer Science) award for best
theoretical paper at ETAPS 2010
Research Description
My primary interest is the development of principled methods to ensure the correctness and security of computer programs. I am best
known for my works in the application of algorithmic learning algorithms to automate formal verification and the design of efficient
algorithms for nite state automata operations. In recent years, I am shifting my research directions to the analysis of real-world programs, in
particular, the veri cation and testing of web program security.
Web program security is a crucial building block of our digital infrastructure. Among other means to ensure cybersecurity, there is an
apparent demand in approaches for automatic web program analysis. String constraint solver is the engine of modern web program testers
and veri ers. There has been a substantial amount of research in recent years on the development of solvers for string constraints. This has
been motivated by numerous application areas such as web security enhancement.
Together with my cooperators from Europe, our team has being working on the problem of string constraint solving since 2014. We
have obtained a series of success in this direction. For example, our string constraint solver Trau [4,5,6] is among the most efficient
implementations in the world. We proposed the first string constraint solving procedure that is able to generate Craig interpolant [1,2],
which is essential in the invariant generation for software model checking. In May 2019, the rst edition of Meeting on String Constraints
and Applications (MOSCA 2019) was held in Bertinoro, Italy. In one week, 43 experts from industry and academia interested in this topic are
invited to present their work and exchange ideas. The participants including researchers from Microsoft, Amazon, and NASA. I am one of
the invitees and will be the organizer of the next edition of MOSCA. I gave two invited tutorials on this topic at international conferences:
CONCUR 2018 (3hrs), SETTA 2019 (2hrs). Our research results are published in CAV 2014, CAV 2015, PLDI 2017, and FMCAD 2018, and PLDI
2020. Those are most inferential venues for formal veri cation and programming language researches.
Publications 6. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen,
Phi-Diep Bui, Julian Dolby, Petr Janku, Hsin-Hung Lin, Lukas
1. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Holik, Wei-Cheng Wu "Efficient Handling of String-Number
Lukás Holík, Ahmed Rezine, Philipp Rümmer, Jari Stenman, Conversion", PLDI 2020.
"String Constraints for Verification", CAV 2014.
7. Yu-Fang Chen, Ondrej Lengal, Tony Tan, Zhilin Wu, "Register
2. Parosh A. Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Lukás automata with linear arithmetic", LICS 2017.
Holík, Ahmed Rezine, Philipp Rümmer, Jari Stenman, "Norn: An
SMT Solver for String Constraints", CAV 2015. 8. Yu-Fang Chen, Lei Song, Zhilin Wu, "The Commutativity
Problem of the MapReduce Framework: A Transducer-Based
3. Fang Yu, Ching-Yuan Shueh, Chun-Han Lin, Yu-Fang Chen, Approach", CAV 2016.
Bow-Yaw Wang, Tevfik Bultan, "Optimal Sanitization Synthesis
for Web Application Vulnerability Repair", ISSTA 2016. 9. Yu-Fang Chen, Matthias Heizmann, Ondrej Lengal, Yong Li,
Ming-Hsien Tsai, Andrea Turrini, Lijun Zhang, "Advanced
4. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Phi-Diep Bui, Automata-based Algorithms for Program Termination Checking",
Yu-Fang Chen, Lukáš Holík, Ahmed Rezine, Philipp Rümmer, PLDI 2018.
"Flatten and Conquer (A Framework for Efficient Analysis of
String Constraints)", PLDI 2017. 10. Yu-Fang Chen, Chiao Hsieh, Ondrej Lengál, Tsung-Ju Lii, Ming-
Hsien Tsai, Bow-Yaw Wang, Farn Wang, "PAC Learning-based
5. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Bui Verification and Model Synthesis", ICSE 2016.
Phi Diep, Lukás Holík, Ahmed Rezine, Philipp Rümmer, "Trau:
SMT solver for string constraints", FMCAD 2018.
172
人 Research Fellow
員 陳郁方 Yu-Fang Chen
Faculty Ph.D., Information Management, National Taiwan University, Taiwan
T +886-2-2788-3799 ext. 1514 E yfc@iis.sinica.edu.tw
F +886-2-2782-4814 W www.iis.sinica.edu.tw/pages/yfc
・ Research Fellow, IIS, Academia Sinica (2018-present)
・ Professor, IM, National Taiwan University (2019)
・ Professor, MIS, National Taipei University (2019-present)
・ Associate Research Fellow, IIS, Academia Sinica (2014-2018)
・ Adjunct Associate Professor, MIS, National Taipei University (2014-2019)
・ Adjunct Assistant Professor, IM, National Taiwan University (2010-2014)
・ Assistant Research Fellow, IIS, Academia Sinica (2009-2014)
・ PostDoc, Uppsala University (2009)
・ EATCS (European Association for Theoretical Computer Science) award for best
theoretical paper at ETAPS 2010
Research Description
My primary interest is the development of principled methods to ensure the correctness and security of computer programs. I am best
known for my works in the application of algorithmic learning algorithms to automate formal verification and the design of efficient
algorithms for nite state automata operations. In recent years, I am shifting my research directions to the analysis of real-world programs, in
particular, the veri cation and testing of web program security.
Web program security is a crucial building block of our digital infrastructure. Among other means to ensure cybersecurity, there is an
apparent demand in approaches for automatic web program analysis. String constraint solver is the engine of modern web program testers
and veri ers. There has been a substantial amount of research in recent years on the development of solvers for string constraints. This has
been motivated by numerous application areas such as web security enhancement.
Together with my cooperators from Europe, our team has being working on the problem of string constraint solving since 2014. We
have obtained a series of success in this direction. For example, our string constraint solver Trau [4,5,6] is among the most efficient
implementations in the world. We proposed the first string constraint solving procedure that is able to generate Craig interpolant [1,2],
which is essential in the invariant generation for software model checking. In May 2019, the rst edition of Meeting on String Constraints
and Applications (MOSCA 2019) was held in Bertinoro, Italy. In one week, 43 experts from industry and academia interested in this topic are
invited to present their work and exchange ideas. The participants including researchers from Microsoft, Amazon, and NASA. I am one of
the invitees and will be the organizer of the next edition of MOSCA. I gave two invited tutorials on this topic at international conferences:
CONCUR 2018 (3hrs), SETTA 2019 (2hrs). Our research results are published in CAV 2014, CAV 2015, PLDI 2017, and FMCAD 2018, and PLDI
2020. Those are most inferential venues for formal veri cation and programming language researches.
Publications 6. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen,
Phi-Diep Bui, Julian Dolby, Petr Janku, Hsin-Hung Lin, Lukas
1. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Holik, Wei-Cheng Wu "Efficient Handling of String-Number
Lukás Holík, Ahmed Rezine, Philipp Rümmer, Jari Stenman, Conversion", PLDI 2020.
"String Constraints for Verification", CAV 2014.
7. Yu-Fang Chen, Ondrej Lengal, Tony Tan, Zhilin Wu, "Register
2. Parosh A. Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Lukás automata with linear arithmetic", LICS 2017.
Holík, Ahmed Rezine, Philipp Rümmer, Jari Stenman, "Norn: An
SMT Solver for String Constraints", CAV 2015. 8. Yu-Fang Chen, Lei Song, Zhilin Wu, "The Commutativity
Problem of the MapReduce Framework: A Transducer-Based
3. Fang Yu, Ching-Yuan Shueh, Chun-Han Lin, Yu-Fang Chen, Approach", CAV 2016.
Bow-Yaw Wang, Tevfik Bultan, "Optimal Sanitization Synthesis
for Web Application Vulnerability Repair", ISSTA 2016. 9. Yu-Fang Chen, Matthias Heizmann, Ondrej Lengal, Yong Li,
Ming-Hsien Tsai, Andrea Turrini, Lijun Zhang, "Advanced
4. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Phi-Diep Bui, Automata-based Algorithms for Program Termination Checking",
Yu-Fang Chen, Lukáš Holík, Ahmed Rezine, Philipp Rümmer, PLDI 2018.
"Flatten and Conquer (A Framework for Efficient Analysis of
String Constraints)", PLDI 2017. 10. Yu-Fang Chen, Chiao Hsieh, Ondrej Lengál, Tsung-Ju Lii, Ming-
Hsien Tsai, Bow-Yaw Wang, Farn Wang, "PAC Learning-based
5. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Bui Verification and Model Synthesis", ICSE 2016.
Phi Diep, Lukás Holík, Ahmed Rezine, Philipp Rümmer, "Trau:
SMT solver for string constraints", FMCAD 2018.
172
