個人資料
蔡益坤
博士 美國加州大學洛杉磯分校 Dept. of Computer Science 博士
碩士 美國加州大學洛杉磯分校 Dept. of Computer Science 碩士
學士 國立臺灣大學資訊工程學系學士
研究室 : 二館 1108
電話 : (02)33661189
傳真 : (02)23698014
E-mail : tsay@ntu.edu.tw
諮詢時段 :
相關連結 :
主要研究領域
• 正規軟體驗證
• 語意化全球資訊網
• 軟體安全
• 時序邏輯與自動機
研究領域摘要
學歷
• 美國加州大學洛杉磯分校 Dept. of Computer Science 博士
• 美國加州大學洛杉磯分校 Dept. of Computer Science 碩士
• 國立臺灣大學資訊工程學系學士
課程
• 演算法
• 自動化軟體驗證
• 資料結構
• 資訊安全
• 軟體開發方法
• 軟體規格與驗證
獲獎
2016  LICS Test-of-Time Award (General Decidability Theorems for Infinite-State Systems, 1996)
經歷
2010/08 – now             Professor, Dept. of Information Management, National Taiwan University, Taiwan
1996/08 – 2010/07       Associate Professor, Dept. of Information Management, National Taiwan University, Taiwan
1995/08 – 1996/07       Lecturer, Dept. of Information Management, National Taiwan University, Taiwan
1993/10 – 1995/07       Postdoctoral Researcher, Dept. of Computer Systems, Uppsala University, Sweden
研討會論文
  1. M.-H. Tsai, Y.-K. Tsay, and Y.-S. Hwang, July 2013, GOAL for Games, Omega-Automata, and Logics, The 25th International Conference on Computer Aided Verification (CAV 2013), LNCS 8044, 883-889, (Saint Petersburg, Russia).
  2. Ming-Hsien Tsai, Seth Fogarty, Moshe Y. Vardi, Yih-Kuen Tsay, May 2012, State of Büchi Complementation, 15th International Conference on Implementation and Application of Automata (CIAA 2010).
  3. Y.-K. Tsay, M.-H. Tsai, J.-S. Chang, and Y.-W. Chang, March 2011, Büchi Store: An Open Repository of Büchi Automata, The 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2011), LNCS 6605, 262-266, Springer, (Saarbrücken, Germany).
  4. M.-H. Tsai, S. Fogarty, M.Y. Vardi and Y.-K. Tsay, January 2011, State of Büchi Complementation, The 15th International Conference on Implementation and Application of Automata (CIAA 2010), LNCS 6482, 261-271, Springer., (Winnipeg, Manitoba, Canada).
  5. Y.-F. Chen, E.M. Clarke, A. Farzan, F. He, M.-H. Tsai, Y.-K. Tsay, B.-Y. Wang, and L. Zhu, October 2010, "Comparing Learning Algorithms in Automated Assume-Guarantee Reasoning," in Leveraging Applications of Formal Methods, Verification, and Validation, The 4th International Symposium on Leveraging Applications (ISoLA 2010), LNCS 6415, 643-657, Springer., (Crete, Greece).
  6. Y.-F. Chen, E.M. Clarke, A. Farzan, M.-H. Tsai, Y.-K. Tsay, and B.-Y. Wang, July 2010, Automated Assume-Guarantee Reasoning through Implicit Learning, The 22nd International Conference on Computer Aided Verification (CAV 2010) LNCS 6174, 511-526, Springer., (Edinburgh, UK).
  7. S. Magill, M.-H. Tsai, P. Lee, and Y.-K. Tsay, January 2010, Automatic Numeric Abstractions for Heap-Manipulating Programs, The 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2010), (Madrid, Spain).
  8. Stephen Magill, Ming-Hsien Tsai, Peter Lee, Yih-Kuen Tsay, December 2010, Numeric Abstractions for Heap-Manipulating Programs, 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2010).
  9. Yu-Fang Chen, Edmund M. Clarke, Azadeh Farzan, Ming-Hsien Tsai, Yih-Kuen Tsay, Bow-Yaw Wang, December 2010, Automated Assume-Guarantee Reasoning through Implicit Learning, Computer Aided Verification, 22nd International Conference (CAV 2010).
  10. Stephen Magill, Ming-Hsien Tsai, Peter Lee, Yih-Kuen Tsay, January 2010, Automatic Numeric Abstractions for Heap-Manipulating Programs, 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2010), (Madrid).
  11. S. Magill, M.-H. Tsai, P. Lee, Y.-K. Tsay, October 2009, Automatic Numeric Abstractions for Heap-Manipulating Programs, Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2010).
  12. Y. -F. Chen, A. Farzan, E. M. Clarke, Y. -K. Tsay, B. -W. Wang, March 2009, Learning Minimal Separating DFA’s for Compositional Verification, Proceedings of the 15th International Conference on Tools and Algorithm for the Construction and Analysis of System (TACAS 2009).
  13. Y. -K. Tsay, Y. -F. Chen, M. -H. Tsai, W. -C. Chan, C. -J. Luo, January 1970, GOAL Extended: Towards a Research Tool for Omega Automata and Temporal Logic, Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2008).
  14. S. Magill, M. -H. Tsai, P. Lee, Y. -K. Tsay, July 2008, THOR: A Tool for Reasoning about Shape and Arithmetic, Proceedings of the 20th International Conference on Computer Aided Verification (CAV 2008).
  15. Y. -K. Tsay, B. -Y. Wang, July 2008, Automated Compositional Reasoning of Intuitionistically Closed Regular Properties, Proceedings of the 13th International Conference on Implementation and Application of Automata (CIAA 2008).
  16. A. Farzan, Y. -F. Chen, E. M. Clarke, Y. -K. Tsay, B. -Y. Wang, January 1970, Extending Automated Compositional Verification to the Full Class of Omega-Regular Languages, Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2008).
  17. Y. -K. Tsay, Y. -F. Chen, M. -H. Tsai, K. -N. Wu, W. -C. Chan, March 2007, GOAL: A Graphical Tool for Manipulating Buchi Automata and Temporal Formulae, Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2007).
  18. Y. -K. Tsay, Y. -F. Chen, K. -N. Wu, August 2006, Tool Support for Learning Büchi Automata and Linear Temporal Logic, The 2006 Formal Methods in the Teaching Lab Workshop (A Workshop at the Formal Methods 2006 Symposium), (Hamilton, Ontario).
  19. J. -W. Teng, Y. -K. Tsay, September 2003, Composing Temporal-Logic Specifications with Machine Assistance, Proceedings of the 12th International Formal Methods Europe Symposium (FME 2003).
  20. 蔡益坤、王佳竣、陳柏均, July 2003, 網路服務撮合系統之設計與實作 - 以旅程計畫為例, 第十四屆國際資訊管理研討會, (Chiayi, Taiwan).
  21. 蔡益坤、饒訓豪、劉智雄, July 2003, 以知識本體為基礎的網路服務媒合方法, 第十四屆國際資訊管理研討會, (Chiayi, Taiwan).
  22. Y. -K. Tsay, March 2000, Compositional Verification in Linear-Time Temporal Logic, Proceedings of the Third International Conference on Foundations of Software Science and Computation Structures.
  23. Y. -K. Tsay, September 1998, Deriving a Scalable Algorithm for Mutual Exclusion, Proceedings of the 12th International Symposium on Distributed Computing (DISC, formerly WDAG).
  24. P. A. Abdulla, K. Cerans, B. Jonsson, Y. -K. Tsay, July 1996, General Decidability Theorems for Infinite-State Systems, Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science (LICS).
  25. B. Jonsson, Y. -K. Tsay, May 1995, Assumption/Guarantee Specifications in Linear-Time Temporal Logic, Proceedings of the 6th International Joint Conference on the Theory and Practice of Software Development (TAPSOFT).
  26. Y. -K. Tsay, R. L. Bagrodia, September 1994, An Algorithm with Optimal Failure Locality for the Dining Philosophers Problem, Proceedings of the 8th International Workshop on Distributed Algorithms (WDAG).
  27. Y. -K. Tsay, R. L. Bagrodia, May 1994, Operational Implication of Conditional UNITY Properties, Proceedings of DIMACS Workshop on Specification of Parallel Algorithms, (Princeton, New Jersey).
  28. Y. -K. Tsay, R. L. Bagrodia, June 1992, A Real-Time Algorithm for Fair Interprocess Synchronization, Proceedings of the 12th International Conference on Distributed Computing Systems (ICDCS).
期刊論文
  1. M.-H. Tsai, S. Fogarty, M.Y. Vardi, and Y.-K. Tsay, January 2014, State of Büchi Complementation, Logical Methods in Computer Science.
  2. Y.-K. Tsay, M.-H. Tsai, J.-S. Chang, Y.-W. Chang, and C.-S. Liu, January 2013, Büchi Store: An Open Repository of ω-Automata, International Journal on Software Tools for Technology Transfer (SCI), Vol 15, Iss 2, Pages 109-123.
  3. Y.-K. Tsay, B.-Y. Wang, August 2009, Automated Compositional Reasoning of Intuitionistically Closed Regular Properties, International Journal of Foundations of Computer Science, 747 - 762.
  4. Y. -K. Tsay, Y. -F. Chen, M. -H. Tsai, K. -N. Wu, W. -C. Chan, C. -J. Luo, J. -S. Chang, May 2009, Tool Support for Learning Buchi Automata and Linear Temporal Logic, Formal Aspects of Computing, 259 - 275.
  5. D. A. Peled, Y. -K. Tsay, February 2007, Automated Technology for Verification and Analysis (ATVA 2005) - Preface, International Journal of Foundations of Computer Science, 1 - 3.
  6. P. A. Abdulla, K. Cerans, B. Jonsson, Y. -K. Tsay, January 2000, Algorithmic Analysis of Programs with Well Quasi-Ordered Domains, Information and Computation, 109 - 127.
  7. B. Jonsson, Y. -K. Tsay, October 1996, Assumption/Guarantee Specifications in Linear-Time Temporal Logic, Theoretical Computer Science, 47 - 72.
  8. Y. -K. Tsay, R. L. Bagrodia, January 1995, Deducing Fairness Properties in UNITY Logic - A New Completeness Result, ACM Transactions on Programming Languages and Systems, 16 - 27.
  9. Y. -K. Tsay, R. L. Bagrodia, July 1994, Fault-Tolerant Algorithms for Fair Interprocess Synchronization, IEEE Transactions on Parallel and Distributed Systems, 737 - 748.
  10. Y. -K. Tsay, R. L. Bagrodia, July 1993, Some Impossibility Results in Interprocess Synchronization, Distributed Computing, 221 - 231.
專書
暫無資料
專書論文
暫無資料
技術報告
暫無資料
其他
暫無資料