Page 112 - untitled
P. 112

ˮݡగ

 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
   107   108   109   110   111   112   113   114   115   116   117