Page 62 - profile2014.indd

研究員
王柏堯 Bow-Yaw Wang

Research Fellow
Ph.D., Computer Science, University of Pennsylvania
Tel: +886-2-2788-3799 ext.1717 Fax: +886-2-2782-4814
Email: bywang@iis.sinica.edu.tw
http://www.iis.sinica.edu.tw/~bywang

● Research Fellow (2012-) Research Description
● Adjunct Associate Professor at

National Taiwan University (2009- My research interests include model checking, automata theory, formal veri cation, and

2012) computational logic. Formal veri cation is a mathematical and logical method that checks
properties about computer systems. Among several techniques in formal veri cation, I am

● Associate Research Fellow (2008- most interested in model checking. Given a formal property and a system description, a
2012) model checker veri es whether the system description conforms to the property. The mod-

● Invited Professor at INRIA (2009- el checking problem in general is computationally hard, I have been developing algorithms

2011) and heuristics to improve the e ciency of model checking. In order to evaluate the ef-

fectiveness of veri cation algorithms, I have implemented the model checker OMOCHA.
● Invited Associate Professor at This model checker supports both BDD- and SAT-based algorithms, and has been used as a
Tsinghua University (2009-2010) research prototype system in the past.
● Adjunct Assistant Professor at In recent years, my research interests have focused on applying algorithmic learning to for-
National Taiwan University (2004- mal veri cation. Consider, for instance, verifying a safety property on a system composed of

2009) several components. Oftentimes, an engineer veri es di erent aspects of the system one at

● Assistant Research Fellow (2003- a time. For each aspect, she speci es a safety property and checks whether relevant system
2008) components work property. Subsequently, only a portion of the system is needed to verify
a safety property. However, it requires system design expertise to identify relevant system
components. For systems with complicated interactions among components, identifying
proper system components can be very time consuming.
One can formulate the aforementioned problem as a learning problem. With existing learning algorithms for Boolean functions, I have

developed a technique to synthesize relevant assumptions for compositional reasoning. The technique can be generalized to di erent

veri cation algorithms and even computation models. More interestingly, the learning-based approach can be generalized to other
problems in formal veri cation. For instance, one can reformulate the problems of generating loop invariants and proving loop termina-

tion as di erent learning problems. Such problems can thus be solved by applying algorithmic learning. The interaction between formal

veri cation and algorithmic learning is in fact reciprocal. Standard learning models may not be the most suitable for formal veri cation.

To improve the e ciency of algorithmic learning, I have also developed an incremental learning algorithm under a learning model in-

spired by applications in formal veri cation.
Publications
1. Fei He, Bow-Yaw Wang, Liangze Yin, and Lei Zhu. Sym- puter Aided Verifi cation (CAV ‘12). Berkeley, USA. July 7-13,
bolic Assume-Guarantee Reasoning through BDD Learning. 2012.
th
36 International Conference on Software Engineering (ICSE
2014), Hyderabad, India, 2014. 7. Wonchan Lee, Bow-Yaw Wang, and Kwangkeun Yi. Termi-
nation Analysis with Algorithmic Learning. 24 International
th
2. Fei He, Liangze Yin, Bow-Yaw Wang, Lianyi Zhang, Guanyu Conference on Computer Aided Verifi cation (CAV ‘12). Berke-
Mu, Wenrui Meng. VCS: A Verifier for Component-Based ley, USA. July 7 - 13, 2012.

Systems. Automated Technology for Verifi cation and Analysis 8. Wenrui Meng, Fei He, Bow-Yaw Wang, and Qiang Liu.
(ATVA 2013), pp 478-481, LNCS 8172, 2013.

Thread-Modular Model Checking with Iterative Refinement.
th
3. Min Zhou, Fei He, Bow-Yaw Wang, Ming Gu, Jiaguang Sun. 4 NASA Formal Methods (NFM ‘12). Norfolk, USA. April

A Unified Framework for DPLL(T) + Certificates. Journal of 3-5, 2012.
Applied Mathematics, (2013). 2013.
9. Yungbum Jung, Wonchan Lee, Bow-Yaw Wang, and Kwang-

4. Wonchan Lee, Yungbum Jung, Bow-Yaw Wang, Kwangkuen keun Yi. Predicate Generation for Learning-Based Quantifier-
Yi. Predicate Generation for Learning-Based Quantifier-Free Free Loop Invariant Inference. 17 International Conference

th
Loop Invariant Inference. Logical Methods in Computer Sci- on Tools and Algorithms forthe Construction and Analysis of
ence 8(3), 2012. Systems (TACAS ‘11). Saarbruecken, Germany. March 28 - 31,
2011.
5. Yu-Fang Chen and Bow-Yaw Wang. BULL: A Library for
Learning Algorithms of Boolean Functions. 19 International 10. Yu-Fang Chen, Edmund M. Clarke, Azadeh Farzan, Fei He,
th
Conference on Tools and Algorithms for the Construction and Ming-Hsien Tsai, Yih-Kuen Tsay, Bow-Yaw Wang, and Lei
Analysis of Systems. Rome, Italy. March, 2013. Zhu. Comparing Learning Algorithms in Automated Assume-
Guarantee Reasoning. 4 International Symposium on Lever-
th
6. Yu-Fang Chen and Bow-Yaw Wang. Learning Boolean Func-
th
tions Incrementally. 24 International Conference on Com- aging Applications of Formal Methods, Verifi cation and Vali-
dation (ISOLA ‘10). Crete, Greece. 18 - 20 October, 2010.
62 研究人員 Research Faculty