個人資料
蔡益坤
博士 美國加州大學洛杉磯分校 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, 2013, GOAL for Games, Omega-Automata, and Logics , The 25th International Conference on Computer Aided Verification (CAV 2013), LNCS 8044, 883-889 , July , (Saint Petersburg, Russia)
  2. Ming-Hsien Tsai, Seth Fogarty, Moshe Y. Vardi, Yih-Kuen Tsay, 2012, State of Büchi Complementation , 15th International Conference on Implementation and Application of Automata (CIAA 2010) , May
  3. Y.-K. Tsay, M.-H. Tsai, J.-S. Chang, and Y.-W. Chang, 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 , March , (Saarbrücken, Germany)
  4. M.-H. Tsai, S. Fogarty, M.Y. Vardi and Y.-K. Tsay, 2011, State of Büchi Complementation , The 15th International Conference on Implementation and Application of Automata (CIAA 2010), LNCS 6482, 261-271, Springer. , January , (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, 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. , October , (Crete, Greece)
  6. Y.-F. Chen, E.M. Clarke, A. Farzan, M.-H. Tsai, Y.-K. Tsay, and B.-Y. Wang, 2010, Automated Assume-Guarantee Reasoning through Implicit Learning , The 22nd International Conference on Computer Aided Verification (CAV 2010) LNCS 6174, 511-526, Springer. , July , (Edinburgh, UK)
  7. S. Magill, M.-H. Tsai, P. Lee, and Y.-K. Tsay, 2010, Automatic Numeric Abstractions for Heap-Manipulating Programs , The 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2010) , January , (Madrid, Spain)
  8. Stephen Magill, Ming-Hsien Tsai, Peter Lee, Yih-Kuen Tsay, 2010, Numeric Abstractions for Heap-Manipulating Programs , 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2010) , December
  9. Yu-Fang Chen, Edmund M. Clarke, Azadeh Farzan, Ming-Hsien Tsai, Yih-Kuen Tsay, Bow-Yaw Wang, 2010, Automated Assume-Guarantee Reasoning through Implicit Learning , Computer Aided Verification, 22nd International Conference (CAV 2010) , December
  10. Stephen Magill, Ming-Hsien Tsai, Peter Lee, Yih-Kuen Tsay, 2010, Automatic Numeric Abstractions for Heap-Manipulating Programs , 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2010) , January , (Madrid)
  11. S. Magill, M.-H. Tsai, P. Lee, Y.-K. Tsay, 2009, Automatic Numeric Abstractions for Heap-Manipulating Programs , Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2010) , October
  12. Y. -F. Chen, A. Farzan, E. M. Clarke, Y. -K. Tsay, B. -W. Wang, 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) , March
  13. Y. -K. Tsay, Y. -F. Chen, M. -H. Tsai, W. -C. Chan, C. -J. Luo, 2008, 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) , January
  14. S. Magill, M. -H. Tsai, P. Lee, Y. -K. Tsay, 2008, THOR: A Tool for Reasoning about Shape and Arithmetic , Proceedings of the 20th International Conference on Computer Aided Verification (CAV 2008) , July
  15. Y. -K. Tsay, B. -Y. Wang, 2008, Automated Compositional Reasoning of Intuitionistically Closed Regular Properties , Proceedings of the 13th International Conference on Implementation and Application of Automata (CIAA 2008) , July
  16. A. Farzan, Y. -F. Chen, E. M. Clarke, Y. -K. Tsay, B. -Y. Wang, 2008, 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) , January
  17. Y. -K. Tsay, Y. -F. Chen, M. -H. Tsai, K. -N. Wu, W. -C. Chan, 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) , March
  18. Y. -K. Tsay, Y. -F. Chen, K. -N. Wu, 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) , August , (Hamilton, Ontario)
  19. J. -W. Teng, Y. -K. Tsay, 2003, Composing Temporal-Logic Specifications with Machine Assistance , Proceedings of the 12th International Formal Methods Europe Symposium (FME 2003) , September
  20. 蔡益坤、王佳竣、陳柏均, 2003, 網路服務撮合系統之設計與實作 - 以旅程計畫為例 , 第十四屆國際資訊管理研討會 , July , (Chiayi, Taiwan)
  21. 蔡益坤、饒訓豪、劉智雄, 2003, 以知識本體為基礎的網路服務媒合方法 , 第十四屆國際資訊管理研討會 , July , (Chiayi, Taiwan)
  22. Y. -K. Tsay, 2000, Compositional Verification in Linear-Time Temporal Logic , Proceedings of the Third International Conference on Foundations of Software Science and Computation Structures , March
  23. Y. -K. Tsay, 1998, Deriving a Scalable Algorithm for Mutual Exclusion , Proceedings of the 12th International Symposium on Distributed Computing (DISC, formerly WDAG) , September
  24. P. A. Abdulla, K. Cerans, B. Jonsson, Y. -K. Tsay, 1996, General Decidability Theorems for Infinite-State Systems , Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science (LICS) , July
  25. B. Jonsson, Y. -K. Tsay, 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) , May
  26. Y. -K. Tsay, R. L. Bagrodia, 1994, An Algorithm with Optimal Failure Locality for the Dining Philosophers Problem , Proceedings of the 8th International Workshop on Distributed Algorithms (WDAG) , September
  27. Y. -K. Tsay, R. L. Bagrodia, 1994, Operational Implication of Conditional UNITY Properties , Proceedings of DIMACS Workshop on Specification of Parallel Algorithms , May , (Princeton, New Jersey)
  28. Y. -K. Tsay, R. L. Bagrodia, 1992, A Real-Time Algorithm for Fair Interprocess Synchronization , Proceedings of the 12th International Conference on Distributed Computing Systems (ICDCS) , June
期刊論文
  1. M.-H. Tsai, S. Fogarty, M.Y. Vardi, and Y.-K. Tsay, 2014, State of Büchi Complementation ,
  2. Y.-K. Tsay, M.-H. Tsai, J.-S. Chang, Y.-W. Chang, and C.-S. Liu, 2013, Büchi Store: An Open Repository of ω-Automata , , Vol 15, Iss 2, Pages 109-123
  3. Y.-K. Tsay, B.-Y. Wang, 2009, Automated Compositional Reasoning of Intuitionistically Closed Regular Properties , , Vol.20 , No.4 , 747 - 762 , ( SCI )
  4. Y. -K. Tsay, Y. -F. Chen, M. -H. Tsai, K. -N. Wu, W. -C. Chan, C. -J. Luo, J. -S. Chang, 2009, Tool Support for Learning Buchi Automata and Linear Temporal Logic , , Vol.21 , No.3 , 259 - 275 , ( SCI )
  5. D. A. Peled, Y. -K. Tsay, 2007, Automated Technology for Verification and Analysis (ATVA 2005) - Preface , , Vol.18 , No.1 , 1 - 3 , ( SCI )
  6. P. A. Abdulla, K. Cerans, B. Jonsson, Y. -K. Tsay, 2000, Algorithmic Analysis of Programs with Well Quasi-Ordered Domains , , Vol.160 , 109 - 127 , ( SCI )
  7. B. Jonsson, Y. -K. Tsay, 1996, Assumption/Guarantee Specifications in Linear-Time Temporal Logic , , Vol.167 , 47 - 72 , ( SCI )
  8. Y. -K. Tsay, R. L. Bagrodia, 1995, Deducing Fairness Properties in UNITY Logic - A New Completeness Result , , Vol.17 , No.1 , 16 - 27 , ( SCI )
  9. Y. -K. Tsay, R. L. Bagrodia, 1994, Fault-Tolerant Algorithms for Fair Interprocess Synchronization , , Vol.5 , No.7 , 737 - 748 , ( SCI )
  10. Y. -K. Tsay, R. L. Bagrodia, 1993, Some Impossibility Results in Interprocess Synchronization , , Vol.6 , No.4 , 221 - 231 , ( SCI )
專書
暫無資料
專書論文
暫無資料
技術報告
暫無資料
其他
暫無資料