Page 111 - untitled
P. 111
ˮݡగ
Wang, Bow-Yaw Ӻᔊʧ Research Description
Research Description
Ӻᔊʧ
ίཀ̘ٙɚɤϋdཥ໘Ⴞп᜕ᗇʊᄿعή͜ For the past two decades, computer aided ysis of infinite-state systems are therefore needed
verification has been widely used in industry. IC for the verification. Developing a proper infinite
ʈุɪfጐཥ༩ணࠇ٫ʊл͜ҖόʈՈԸਈ designers are using formal verification tools to de- model and verifying it are the topics of this line of
˼ࡁணࠇʕٙ፹ႬfһεٙόணࠇࢪɰԴ͜Җό tect errors in their designs. More programmers are my research.
using formal modeling tools to analyze system ar-
ᅼۨʈՈԸʱؓӻ୕ݖfҢٙӺʈЪ݊೯࢝ί III.cDeveloping verification tools. I am also
chitectures. My work is to develop new techniques
ཥ໘Ⴞп᜕ᗇɪอٙҦஔfһᆽʲήႭdҢͦۃٙ in computer aided verification. Specifically, my cur- developing a model checker called OMocha to real-
ize the theoretical investigation. OMocha is written
Ӻ̙ʱމɨΐɧࡈධͦj rent research consists of the following three areas:
in Objective Caml. It has both BDD- and SAT-based Research Fellows
I.cModel checking algorithms. Model check- algorithms. The software architecture allows pro-
I. ᅼۨᏨ᜕စၑج{Ңࡁʊٝ༸ᅼۨᏨ᜕ਪ
ing problem is known to have intractable complex- grammers to develop and combine both techniques
ᕚϞʔ̙дٙልᕏܓfΪϤცࠅ઼೯όٙ˙جԸ ity. Therefore heuristics are needed to tackle real- easily. I hope it will be a research platform for ex-
world problems. BDD-based algorithms are fast perimenting various model checking algorithms.
༆Ӕॆྼ˰ޢʕٙਪᕚfɚʩӔ֛ྡ(BDD)ᗳٙစ
but space-consuming. In recent years, SAT-based
ၑجڢ੬ҞШঃ൬˄εٙাኳfί௰ڐவ verification algorithms have shown some promises. IV.cSystem on Chip (SoC) verification meth-
Research Fellows
ਿ ͉ ༟ ࣘ
ਿ ͉ ༟ ࣘ ϋd˸တԑ̺؍ၑό(SAT)މ˴᜕ٙᗇစၑجɰ Since none of these techniques is always superior odology. SoC designs are known to be error-prone
to the other, more investigations on the relation and because both hardware and software need be inte-
နաՑٵ֛fΪމՉʕӚϞɓ၇˙جˢ̤ɓ၇λd grated. Hardware and software designers are accus-
ᔖcc၈j пӺࡰ interaction between both techniques are of my inter- tomed to different verification and debugging tools.
ҢٙӺ˙ΣഹࠠίઞীՇ٫ʘගٙᗫڷ˸ʿʝਗ est.
Assistant Research Fellow (2003-) As a result, software and hardware components are
ٙઋҖf
௰৷ኪዝj Ph.D., Computer and Information II.cInfinite-state verification. Many infinite- constructed and analyzed separately, their integra-
Science, University of Pennsylvania II. ೌًࠢ࿒᜕ٙᗇ{މəʱؓཥ໘ӻ୕d state models have been proposed to analyze com- tion is hard to achieve. Developing an integrated
(2001) puter systems. These models are most suitable for verification methodology and tool for SoC designs
εೌًࠢ࿒ٙᅼۨʊ̈ԸfவԬᅼۨڢ੬ቇ software systems. However, infinity often leads to is another topic of my research.
ཥcc༑j+886-2-2788-3799 ext. 1717 undecidable results. Abstraction technique and anal-
Υ͜ழӻ୕fʔཀdೌًࠢ࿒ኬߧʔ̙༆
ෂccॆj+886-2-2782-4814 ʘഐሞfΪϤdމə᜕ᗇdҢࡁცࠅפʷٙҦஔ Selected Publications
Selected Publications
ཥɿڦᇌjbywang@iis.sinica.edu.tw ձೌًࠢ࿒ӻ୕ٙʱؓfνО೯࢝ɓࡈቇٙೌࠢ
1. Hsu-Chun Yen, Bow-Yaw Wang, and Ming-Sheng Yang. Some Com- 9. Fang Yu, Bow-Yaw Wang, and Yao-Wen Huang. Bounded Model
ၣccࠫjhttp://www.iis.sinica.edu.tw/pages/bywang ً࿒ᅼۨԨ᜕ᗇʘd݊Ңίவ˙ࠦӺٙ༩ᇞf plexity Results for Rings of Petri Nets. International Journal of Foun- Checking for Region Automata. Joint International Conferences on
dations of Computer Science. Vol. 5 No. 3&4, 1994, pp. 281-292. Formal Modeling and Analysis of Timed Systems (FORMATS) and
III. ೯᜕࢝ᗇʈՈ{Ңͦۃɰ͍ί೯࢝ɓࢁᅼ 2. Hsu-Chun Yen, Bow-Yaw Wang, and Ming-Sheng Yang. Deciding a Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRT-
• Assistant Professor, Information Management, Class of Path Formulas for Conflict-Free Petri Nets Theory of Comput- FT). Grenoble, France, September 2004.
ۨᏨ᜕ʈՈḍਂ OMochad˸کྼБଣሞઞী ing Systems , 30(5):475-494, September/October 1997. 10. Fang Yu and Bow-Yaw Wang. Toward Unbounded Model Checking
National Taiwan University (2004-), 3. Rajeev Alur and Bow-Yaw Wang. ``Next'' Heuristic for On-the-fly for Region Automata. 2nd International Symposium on Automated
ٙഐ؈fOMocha ݊˸ Objectvie Caml ԸᄳЪϾϓ
• Assistant Research Fellow, Academia Sinica (2003-), Model Checking CONCUR '99: Concurrency Theory, Tenth Interna- Technology for Verifi cation and Analysis. Taipei, Taiwan, November
ٙf̴ΝࣛኹϞ˸ɚʩӔ֛ྡձတԑ̺؍ၑόމݖ tional Conference. LNCS 1664 , 98-113, 1999. 2004.
• Senior Software Engineer, Verplex Inc. (2001-2003), 4. Bow-Yaw Wang, Jose Meseguer, and Carl A. Gunter. Specifi cation and 11. Bow-Yaw Wang. Specification of an Infinite-State Local Model
ٙစၑجfՉழݖʪόணࠇࢪ˙کή೯ formal verification of a PLAN algorithm in Maude. Proceedings of the Checker in Rewriting Logic. The Seventeenth International Confer-
• Ph.D., Computer and Information Science, 2000 ICDCS workshop on Distributed System Validation and Verifi ca- ence on Software Engineering and Knowledge Engineering. Taipei,
࢝ʿΥԻவՇ၇ҦஔfҢҎૐਗ਼Ըவࡈӻ୕ঐϓމ
University of Pennsylvania (2001), tion, IEEE Computer Society. April 2000. Taiwan. July 14-16, 2005.
ɓࡈ༊᜕ʔΝᅼ᜕ۨᗇစၑجٙӺ̨̻f 5. Rajeev Alur, Grosu Radu and Bow-Yaw Wang. Automated Refi nement 12. Bow-Yaw Wang. Proving \forall\mu-Calculus Properties with SAT-
• M.S., Electrical Engineering, National Taiwan Checking for Asynchronous Processes Formal Methods in Computer Based Model Checking. 25th IFIP WG 6.1 International Conference
University (1994), IV. ӻ୕౺˪ʘ᜕ᗇ˙ج{͟ழேცࠅ Aided Design (FMCAD00) . Austin, Texas, November 1-3, 2000. on Formal Techniques for Networked and Distributed Systems. Taipei,
6. Rajeev Alur and Bow-Yaw Wang. Verifying Network Protocol Imple- Taiwan. October 2-5, 2005.
• B.S., Mathematics, National Taiwan University Υٙᇝ݂dҢࡁٝ༸ӻ୕౺˪ٙணࠇପ͛፹ mentations by Symbolic Refi nement Checking Computer Aided Verifi - 13. Bow-Yaw Wang. Automatic Verification of a Model Checker by Re-
(1992) Ⴌfணࠇࢪձழʈࢪ୦࿕ʔΝ᜕ٙᗇձ 7. cation (CAV '01) . Paris, France, July 18-23, 2001. th fl ection. Eighth International Symposium on Practical Aspects of De-
Bow-Yaw Wang. Mu-Calculus Model Checking in Maude. 5 Interna-
clarative Languages. Charleston, South Carolina, USA. January 9-10,
ਈ፹ʈՈdΪϤdழʩ݊йήܔͭ˸ʿʱ tional Workshop on Rewriting Logic and its Applications. Barcelona, 2006.
Spain. March 27-28, 2004. 14. Bow-Yaw Wang. Modeling and Analyzing Applications with Domain-
ؓdϾ̴ࡁٙΥఱʔ༺ϓfމӻ୕౺˪೯࢝ɓ 8. F. Wang, K. Schmidt, F. Yu, G.D. Huang, and B.-Y. Wang. BDD-Based Specific Languages by Reflective Rewriting: A Case Study. 21 Annual
st
Safety-Analysis of Concurrent Software with Pointer Data Structures ACM Symposium on Applied Computing. Dijon, France. April 23-27,
ࢁΥ᜕ٙᗇ˙جձʈՈɰ݊Ң̤ɓධӺ˙Σf
Using Graph Automorphism Symmetry Reduction. IEEE Transactions 2006.
on Software Engineering, 30(6), June 2004.
100 101
