Page 61 - profile-ok

研究人員 ｜ Research Faculty

● Adjoint Associate Professor, Information Management, National
王柏堯 Bow-Yaw Wang Taiwan University (2009-)
● Associate Research Fellow, IIS, Academia Sinica (2008-)
● Adjoint Assistant Professor, Information Management, National
Taiwan University (2004-)
副研究員 Associate Research Fellow ● Assistant Research Fellow, IIS, Academia Sinica (2003-)
Ph.D., Computer Science, University of Pennsylvania ● Senior Software Engineer, Verplex Systems (2001-2003)
● Ph.D., Computer Science, University of Pennsylvania (1995-2001)
Tel: +886-2-2788-3799 ext.1717 ● Research Assistant, IIS, Academia Sinica (1994-1995)
Fax: +886-2-2782-4814 ● M.S., Electrical Engineering, National Taiwan University (1992-1994)
Email: bywang@iis.sinica.edu.tw ● B.S., Mathematics, National Taiwan University (1988-1992)
http://www.iis.sinica.edu.tw/~bywang

建於各種不同的定理證明程式中。不過，一旦時態邏輯或計算模型在各別應用 should different temporal logic or computational model be used in spe- reuse our formalization, one only needs to establish these assumptions
中改變，這個正規化工作則必須重新於執行。我們為 CTL* 進行模組式的正規 cific application. We develop a modular formalization of CTL* to address formally. Using our modular formalization, we have established most of
化，以解決此一問題。CTL* 比 linear temporal logic 和 computation tree logic 還 the problem. CTL* is strictly more expressive than both linear temporal the soundness theorems for LTL, UB, CTL, and CTL*. Due to our modular
要具表現性。除此之外，這個模組式的正規化於Coq的模組系統中，明確地說明 logic and computation tree logic. Moreover, our modular formalization formalization, these theorems need not be re-established when they are
計算假設。若要重覆使用這個正規化，使用者只須正規地建立這些假設。利用 states computation assumptions explicitly in the Coq module system. To instantiated in future applications.
我們模組式的正規化，我們已經證明大部份的 LTL，UB，CTL 和 CTL* 正確性定
理。而由於模組化，這些證明在未來的應用中，無須被重新建立即可被使用。
研究簡介
代表著作 Publications
模型檢驗和自動定理證明是正規驗證中，兩種最具潛力 Research Description
的技術。在模型檢驗中，電腦系統的數學模型針對其正
規規格進行檢查。這個以模型理論為基礎的技術能有效 Model checking and theorem proving are two of the most promising techniques in 1. Hsu-Chun Yen, Bow-Yaw Wang, and Ming-Sheng Yang. Some flection. 8 International Symposium on Practical Aspects of Declar-
th
率地探索有限狀態模型，並已被廣泛地應用於電腦硬體 formal verification. In model checking, a mathematical model of computer system Complexity Results for Rings of Petri Nets. International Journal of ative Languages. Charleston, South Carolina, USA. January 9-10,
系統的設計。另一方面，電腦系統則在自動定理證明技 is checked against its formal requirements. The model-theoretic technique is able Foundations of Computer Science. 3/4(5):281-292, 1994. 2006.
術中被正規化為邏輯理論。系統之驗證則等同自這些邏 to explore finite-state models rather efficiently and widely applied in the design of 2. Hsu-Chun Yen, Bow-Yaw Wang, and Ming-Sheng Yang. Deciding a 14. Bow-Yaw Wang. Modeling and Analyzing Applications with Do-
輯理論推導數學定理。這個以證明理論為基礎的技術能 computer hardware systems. On the other hand, computer systems are formalized Class of Path Formulas for Conflict-Free Petri Nets. Theory of Com- main-Specific Languages by Reflective Rewriting: a Case Study. 21 st
正規地檢查數學證明。而由於自動定理證強大的表現能 as logical theories in theorem proving. Verification of systems amounts to deducing puting Systems, 30(5):475-494. September/October 1997. ACM Symposium on Applied Computing. Dijon, France. April 23-27,
力，它被廣泛地運用於如電腦軟體系統等無限狀態系統 mathematical theorems from these logical theories. The proof-theoretic technique 3. Rajeev Alur and Bow-Yaw Wang. “Next” Heuristic for On-the-fly 2006.
is able to check mathematical proofs formally. Due to the expressiveness of theorem
th
之驗證。上述兩種技術各有其優劣，沒有任何一種得以 proving, it is generally used in infinite-state systems such as computer software sys- Model Checking. 10 International Conference on Concurrency The- 15. Bow-Yaw Wang. On the Satisfiability of Modular Arithmetic Formu-
th
令人滿意地驗證任意的電腦系統。因此，如何結合此兩 tems. Either technique has its strength and weakness. Neither can verify arbitrary ory (CONCUR ’99). 1999. lae. 4 Automated Technology for Verification and Analysis. Beijing,
China. October, 2006.
種技術，以發展混合的新技巧，則是一項相當有趣的研 computer systems satisfactorily. One of the most exciting research problems is 4. Bow-Yaw Wang, Jose Meseguer, and Carl A. Gunter. Specification
究問題。 therefore to develop a hybrid technique which combines advantages of both tech- and formal verification of a PLAN algorithm in Maude. 2000 ICDCS 16. Ming-Hsien Tsai and Bow-Yaw Wang. Formalization of CTL* in the
th
Calculus of Inductive Constructions. 11 Annual Asian Computing
workshop on Distributed System Validation and Verification. IEEE
niques. Computer Society, April 2000. Science Conference (ASIAN ’06). Tokyo, Japan. December 6-8, 2006.
我的研究興趣包含了在正規驗證中模型檢驗和自動定理
證明兩項技術。在模型檢驗方面，我們基於證明理論 My research interests include both model checking and theorem proving tech- 5. Rajeev Alur, Grosu Radu, and Bow-Yaw Wang. Automated Refine- 17. Ming-Hsien Tsai and Bow-Yaw Wang. Modular Formalization of Re-
th
架構上，發展了一個完備的模型檢驗演算法。在此架構 niques in formal verification. In model checking, we developed a complete SAT- ment Checking for Asynchronous Processes. Formal Methods in active Modules in Coq. 11 Annual Asian Computing Science Confer-
ence (ASIAN ’06). Tokyo, Japan. December 6-8, 2006.
Computer Aided Design (FMCAD ’00). Austin Texas, November 1-3,
上，模型檢驗演算法成了證明搜尋。而我們的模型檢驗 based model checking algorithm based on a proof-theoretic framework. The model 2000.
演算法則利用先進的 SAT 引擎以搜尋證明，也解決了模 checking algorithm is reduced to proof search in the framework. Our SAT-based 6. Rajeev Alur and Bow-Yaw Wang. Verifying Network Protocol Im- 18. Bow-Yaw Wang. Automatic Derivation of Compositional Rules in
algorithm uses modern SAT solvers to search proofs and hence solve the model
th
Automated Compositional Reasoning. 18 International Conference
型檢驗問題。這個證明理論為基礎的方法，事實上比傳 checking problem. Our proof-theoretic approach is in fact more general than typical plementations by Symbolic Refinement Checking. Computer Aided on Concurrency Theory (CONCUR ’07). Lisbon, Portugal. Septem-
統以利用 SAT 引擎的模型檢驗演算法更為廣泛。首先， SAT-based model checking. Firstly, the new approach is able to verify properties in Verification (CAV ’01). Paris, France. July 18-23, 2001. ber 3-8, 2007.
新的方法能驗證比傳統方法還更具表現能力的邏輯。其 the universal fragment of mu-calculus which is more expressive than the universal 7. R. Alur, L. De Alfaro, R. Grosu, T. A. Henzinger, M. Kang, R. Ma- 19. Geng-Dian Huang and Bow-Yaw Wang. Complete SAT-based Model
次，它已被應用於驗證 context-free processes。我們的 fragment of CTL* and hence linear temporal logic. Secondly, it has been applied jumdar, F. Mang, C. M. Kersch, and B.-Y. Wang. Mocha: A model Checking for Context-Free Processes. 5 International Symposium
th
rd
方法不只能檢驗更多的性質，還能檢驗無限狀態的系 to the verification of context-free processes almost straightforwardly. Our approach checking tool that exploits design structure. 23 International Con- on Automated Technology for Verification and Analysis (ATVA ’07).
統。傳統利用 SAT 引擎的技術，尚未能達同時被推廣於 can not only verify more properties but also infinite-state systems. Traditional SAT- ference on Software Engineering. pp. 835-835, 2001. Tokyo, Japan. October 22-25, 2007.
th
此二方面。 based technique has yet to be generalized in both accounts. 8. Bow-Yaw Wang. Mu-Calculus Model Checking in Maude. 5 Inter- 20. Azadeh Farzon, Yu-Fang Chen, Edmund M. Clarke, Yih-Kuen Tsay,
national Workshop on Rewriting Logic and its Applications (WRLA and Bow-Yaw Wang. Extending Automated Compositional Verifica-
th
組合式分析是減低狀態爆炸問題中，最有效的方法之 Compositional reasoning is one of the most effective techniques to alleviate the ’04). Barcelona, Spain. March 27-28, 2004. tion to the Full Class of Omega-Regular Languages. 14 Interna-
一。在組合式分析中，系統之驗證依證明規則而分解成 state explosion problem in model checking. In compositional reasoning, the verifi- 9. Fang Yu, Bow-Yaw Wang, and Yao-Wen Huang. Bounded Model tional Conference on Tools and Algorithms for the Construction and
Analysis of Systems (TACAS ‘08). Budapest, Hungary. March 29 -
若干關於組成份子之驗證工作。藉由組合證明規則之正 cation of a system is decomposed into simpler verification tasks of its components Checking for Region Automata. Joint International Conferences on April 6, 2008.
according to certain proof rules. By the soundness of compositional proof rules, the
確性，系統之正確性可由其組成份子之正確性而得之。 correctness of the system follows from the correctness of its components. Since Formal Modeling and Analysis of Timed Systems (FORMATS) and 21. Yih-Kuen Tsay and Bow-Yaw Wang. Automated Compositional Rea-
Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRT-
由於各組成份子可各自被驗證，狀態爆炸問題因此而被 components are verified separately, the state explosion problem is therefore circum- FT). Grenoble, France. September 2004. soning of Intuitionistically Closed Regular Properties. 13 Interna-
th
避免。但是發展正確的組合證明規則，卻依賴於性質和 vented. Developing sound compositional proof rules however depends on proper- 10. Fang Yu and Bow-Yaw Wang. Toward Unbounded Model Checking tional Conference on Implementation and Application of Automata
計算模型。事實上，過去數十年來，許多的研究已投入 ties and computational models. Indeed, significant research effort has been devoted for Region Automata. 2 International Symposium on Automated (CIAA ‘08). San Francisco, USA. July 21-24, 2008.
nd
此項工作。針對有限狀態自動機和軌跡語意，我們發展 to it for decades. For finite-state automata and trace semantics, we have developed Technology for Verification and Analysis. Taipei, Taiwan. November 22. Yu-Fang Chen, Azadeh Farzon, Edmund M. Clarke, Yih-Kuen Tsay,
了一套自動化的技術，得以推導組合證明規則。除此以 an automated technique to derive compositional proof rules. Moreover, we have 2004. and Bow-Yaw Wang. Learning Minimal Separating DFA’s for Com-
th
外，我們還證明了 prefix-closed 規則語言形成 Heyting shown that the class of prefix-closed regular languages forms a Heyting algebra. 11. Bow-Yaw Wang. Specification of an Infinite-State Local Model positional Verification. 15 International Conference on Tools and Al-
gorithms for the Construction and Analysis of Systems (TACAS ‘09).
th
代數。因此，直觀邏輯的證明系統 LJ 可以推導在此類規 The proof system LJ for intuitionistic logic is thus able to derive compositional proof Checker in Rewriting Logic. 7 International Conference on Soft- York, UK. March 23 - March 26, 2009.
則語言所適用之組合證明規則。 rules for the subclass of regular languages. ware Engineering and Knowledge Engineering. Taipei, Taiwan. July
14-16, 2005. 23. Yungbum Jung, Soonho Kong, Bow-Yaw Wang, and Kwangkeun Yi.
The very first step in applying theorem proving is to formalize problems in the Deriving Invariants by Algorithmic Learning, Decision Procedures,
在應用自動定理證明的第一步驟，是在所使用之證明程 12. Bow-Yaw Wang. Proving ∀μ-Calculus Properties with SAT-based th
th
式中正規化問題。於正規驗證中，吾人必須將不同的 chosen prover. In formal verification, one has to embed various temporal logics Model Checking. 25 IFIP WG 6.1 International Conference on For- and Predicate Abstraction. 11 International Conference on Verifica-
tion, Model Checking and Abstract Interpretation (VMCAI ‘10). Ma-
and computational models in a prover and carry out proofs formally. Indeed, both
時態邏輯和計算模型建入，並實行正規定理證明。事實 linear temporal logic and computation tree logic has been embedded in various mal Techniques for Networked and Distributed Systems. Taipei, Tai- drid, Spain. January 17 - January 19, 2010.
上，linear temporal logic 和 computation tree logic 已被 theorem provers. However, the formalization task needs to be carried out again wan. October 2-5, 2005.
13. Bow-Yaw Wang. Automatic Verification of a Model Checker by Re-
60 61