Page 81 - profile2014.indd

Sheng-Wei Chen
陳昇瑋 陳郁方 Yu-Fang ChenChen
副研究員 副研究員

Associate Research Fellow
Ph.D, Informational Management, National Taiwan University
Tel: +886-2-2788-3799 ext. 1514 Fax: +886-2-2782-4814
Email: yfc@iis.sinica.edu.tw
http://www.iis.sinica.edu.tw/pages/yfc/index_en.html

Research Description ● Assistant Research Fellow, IIS,
Academia Sinica, 2009-
My primary research interest is to develop automatic tools that can help system developers ● Assistant Professor (Joint Ap-
to ensure the quality of hardware and software designs or algorithms that can be used in pointment), IM, National Taiwan
these tools. In particular, I am interested in the model checking technique and its appli- University, 2012-

cation in software veri cation. Model checking is a fully automatic veri cation technique ● The EATCS (European Association

for state-transition systems. This technique has been used successfully to analyze the com- for Theoretical Computer Sci-
puter hardware and communication protocols and is getting more and more popular in ence) award for best theoretical
verifying computer software. A model checker performs an exhaustive search to determine paper at ETAPS 2010
if systems are correct with respect to given speci cations. In those cases where the speci - ● B.S., BA, National Taiwan Univer-

cation does not hold, the model checker produces a counterexample execution trace. This sity
feature is very useful for nding obscure errors in complex systems. ● M.B.A, IM, National Taiwan Uni-

versity
Most of the researches of model checking focus on two issues: more expressive models for

describing advanced system features (e.g., di erent data types, the shape of heap cells) or ● PhD. IM, National Taiwan Uni-
versity
heuristics to improve the performance of the model checking algorithms. I am interested in
both directions and have been worked on several related projects.
To name a few, our group developed di erent x-point computation procedures based on

algorithmic learning algorithms, which solve several very di cult veri cation tasks. As side products, we found several new algorithmic

learning algorithms, including one for the full class of omega regular language. We are the rst group introducing Boolean learning

algorithm to this eld and developed an incremental version that suits various applications in program veri cation.

Publications
1. Yu-Fang Chen and Bow-Yaw Wang, “BULL: a Library for 8. Yu-Fang Chen, Edmund M. Clarke, Azadeh Farzan, Ming-
Learning Algorithms of Boolean Functions,” TACAS 2013 Hsien Tsai, Yih-Kuen Tsay, and Bow-Yaw Wang, “Automated
Assume-Guarantee Reasoning through Implicit Learning,”
2. Parosh Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Carl CAV 2010
Leonardsson and Ahmed Rezine, “Memorax: Fence Inference
under the TSO Memory Model,” TACAS 2013 9. P.A. Abdulla, Y.-F. Chen, L.o Clemente, L. Holik, C.-D. Hong,
R. Mayr, and T. Vojnar, “Simulation Subsumption in Ramsey-
3. Parosh Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Carl based B uchi Automata Universality and Inclusion Testing,”
Leonardsson and Ahmed Rezine, “Automatic Fence Insertion CAV 2010
in Integer Programs via Predicate Abstraction,” SAS 2012
10. P.A. Abdulla, Y.-F. Chen, L. Holik, R. Mayr and T. Vojnar,
4. Yu-Fang Chen and Bow-Yaw Wang, “Learning Boolean Func-
“When Simulation Meets Antichain (on Language Inclusion
tions Incrementally,” CAV 2012
Checking of NFA/TA) (Best Paper Award),” TACAS 2010
5. Parosh Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Carl
Leonardsson and Ahmed Rezine, “Counter-Example Guided
Fence Insertion under TSO,” TACAS 2012
6. Parosh Abdulla, Yu-Fang Chen, Lorenzo Clemente, Lukas Ho-
lik, Chih-Duo Hong, Richard Mayr, Tomas Vojnar, “Advanced
Ramsey-based Buchi Automata Inclusion Testing,” CONCUR
2011
7. Parosh Abdulla , Yu-Fang Chen, Giorgio Delzanno, Fred-
eric Haziza, Chih-Duo Hong and Ahmed Rezine., “Con-
strained Monotonic Abstraction: a CEGAR for Parameterized

Verification,”CONCUR 2010

81