Page 99 - profile-ok
P. 99
研究人員 ｜ Research Faculty
● Visiting Student, Carnegie Mellon University. 2007~2008, 18 months ACADEMIC HONORS AND AWARDS:
陳郁方 Yu-Fang Chen in total. Recipient of the European Joint Conferences on Theory and Practice
● PostDoc, Uppsala University, Sweden, 2009/5~2009/10 of Software (ETAPS) Scholarship, 2007, 2008, and 2009
● Visiting Researcher, Uppsala University, Sweden, 2010/2~2010/4
● Assistant Research Fellow, IIS, 2009/10~
助研究員 Assistant 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
代表著作 Publications
1. Y.-K. Tsay, Y.-F. Chen, M.-H. Tsai, K.-N. Wu, and W.-C. Chan,
“GOAL: A Graphical Tool for Manipulating Buechi Automata and
研究簡介 Research Description Temporal Formulae,” The 13th International Conference on Tools and
Algorithms for the Construction and Analysis of Systems (TACAS
2007), Lecture Notes in Computer Science, 4424, pages 466--471,
我主要的研究興趣在自動化驗證軟硬體系統正確性的技 My main research interest is on automatic techniques (model checking) for verifying 2007.
術。主要有興趣的方法是模型驗證。在過去數年中，我 correctness of software/hardware system. In the past few years, the main focus is on 2. A. Farzan, Y.-F. Chen, E.M. Clarke, Y.-K. Tsay, and B.-Y. Wang, “Ex-
的主要研究重點包括(1)自動化組合式驗證及，(2)以自動 two topics: (1) automated compositional verification and (2) automata-based model tending Automated Compositional Verification to the Full Class of
機為基礎的模型驗證。自動化組合式驗證的目標是用” checking. The goal of automated compositional verification is to improve the scal- Omega-Regular Languages,” The 14th International Conference on
各個擊破”的方式，透過機器學習演算法，把一個複雜 ability of model checking. In the approach, one applies a compositional inference Tools and Algorithms for the Construction and Analysis of Systems
的驗證問題，自動拆解成數個簡單的子問題。問題的拆 (TACAS 2008), Lecture Notes in Computer Science, 4963, pages 2--
解通常是透過所謂的保證-假設式推論規則。過去我們 rule to break the task of verifying a system down to the subtasks of verifying its 17, 2008.
提出了許多改善自動化組合式驗證的技巧，其中包含了 components. The compositional inference rule is usually in the so-called assume- 3. Y.-K. Tsay, Y.-F. Chen, M.-H. Tsai, W.-C. Chan, and C.-J. Luo,
將他擴充至能驗證活性性質，及能找出一個保證-假設 guarantee style. In the past few years, we proposed several approaches to improve “GOAL Extended: Towards a Research Tool for Omega Automata
and Temporal Logic,” The 14th International Conference on Tools and
式推論規則中最佳環境假設的演算法。相對於 LTL 模型 automated compositional verification, which include extending it to allow the veri- Algorithms for the Construction and Analysis of Systems (TACAS
驗證技術(利用邏輯算式來描述所需要的性質)，以自動 fication of liveness property and a new algorithm that guarantees finding the mini- 2008), Lecture Notes in Computer Science, 4963, pages 346--350,
機為基礎的模型驗證技術允許利用狀態機來描述想要驗 mal contextual assumption of an assume-guarantee rule. In contrast to LTL model 2008.
證的性質。這是一個研發中的方法，有很多問題都還尚 checking that uses a logic formula to describe the desired property, automata-based 4. Y.-F. Chen, A. Farzan, E.M. Clarke, Y.-K. Tsay, and B.-Y. Wang,
待解決(特別是其擴充性)。在去年，我們對於數種不同 model checking allows the use of finite-state machines to describe the property to “Learning Minimal Separating DFA’s for Compositional Verifica-
的自動機，提出了有效率的演算法來最小化一個自動機 be verified. This is an on-going research area; many problems remain there to be tion,” The 15th International Conference on Tools and Algorithms for
the Construction and Analysis of Systems (TACAS 2009), Lecture
及檢測一個自動機的語言是否為另一個自動機的母集。 solved. Notes in Computer Science, 5505, pages 31-45, 2009.
這些演算法對於改善以自動機為基礎的模型驗證都具有 Scalability is still the main concern. In the previous year, we developed efficient al-
相當的重要性。 gorithm for minimizing and checking language inclusion of different types of au- 5. P.A. Abdulla, Y.-F. Chen, L. Holik, and T. Vojnar, “Mediating for Re-
duction (on Minimizing Alternating Buchi Automata),” The 29th An-
tomata, which can be used to improve automate-based model checking. nual Conference on Foundations of Software Technology and Theo-
retical Computer Science (FSTTCS 2009), 2009.
6. Y.-K. Tsay, Y.-F. Chen, M.-H. Tsai, K.-N. Wu, W.-C. Chan, C.-J. Luo,
and J.-S. Chang, “Tool Support for Learning Buechi Automata and
Linear Temporal Logic,” Formal Aspects of Computing, volume 21,
pages 259-275, 2009.
7. P. Abdulla, Y.-F. Chen, L. Holik, R. Mayr and T. Vojnar “When Simu-
lation Meets Antichains (on Checking Language Inclusion of NFA/
TA’s)” The 16th International Conference on Tools and Algorithms
for the Construction and Analysis of Systems (TACAS 2010), Lecture
Notes in Computer Science, 2010.
98 99
