個人資料
蔡益坤
博士 美國加州大學洛杉磯分校 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 July , 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, 2012 May , 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, 2011 March , 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, 2011 January , 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, 2010 October , "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, 2010 July , 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, 2010 January , 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, 2010 December , 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, 2010 December , 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, 2010 January , 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, 2009 October , 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, 2009 March , 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, 2008 January , 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, 2008 July , 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, 2008 July , 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, 2008 January , 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, 2007 March , 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, 2006 August , 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, 2003 September , Composing Temporal-Logic Specifications with Machine Assistance, Proceedings of the 12th International Formal Methods Europe Symposium (FME 2003)
  20. 蔡益坤、王佳竣、陳柏均, 2003 July , 網路服務撮合系統之設計與實作 - 以旅程計畫為例, 第十四屆國際資訊管理研討會 , (Chiayi, Taiwan)
  21. 蔡益坤、饒訓豪、劉智雄, 2003 July , 以知識本體為基礎的網路服務媒合方法, 第十四屆國際資訊管理研討會 , (Chiayi, Taiwan)
  22. Y. -K. Tsay, 2000 March , 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, 1998 September , 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, 1996 July , 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, 1995 May , 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, 1994 September , 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, 1994 May , 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, 1992 June , 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, 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, 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, 2009, Automated Compositional Reasoning of Intuitionistically Closed Regular Properties , International Journal of Foundations of Computer Science , 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 , Formal Aspects of Computing , Vol.21 , No.3 , 259 - 275 , ( SCI )
  5. D. A. Peled, Y. -K. Tsay, 2007, Automated Technology for Verification and Analysis (ATVA 2005) - Preface , International Journal of Foundations of Computer Science , 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 , Information and Computation , Vol.160 , 109 - 127 , ( SCI )
  7. B. Jonsson, Y. -K. Tsay, 1996, Assumption/Guarantee Specifications in Linear-Time Temporal Logic , Theoretical Computer Science , Vol.167 , 47 - 72 , ( SCI )
  8. Y. -K. Tsay, R. L. Bagrodia, 1995, Deducing Fairness Properties in UNITY Logic - A New Completeness Result , ACM Transactions on Programming Languages and Systems , Vol.17 , No.1 , 16 - 27 , ( SCI )
  9. Y. -K. Tsay, R. L. Bagrodia, 1994, Fault-Tolerant Algorithms for Fair Interprocess Synchronization , IEEE Transactions on Parallel and Distributed Systems , Vol.5 , No.7 , 737 - 748 , ( SCI )
  10. Y. -K. Tsay, R. L. Bagrodia, 1993, Some Impossibility Results in Interprocess Synchronization , Distributed Computing , Vol.6 , No.4 , 221 - 231 , ( SCI )
專書
暫無資料
專書論文
暫無資料
技術報告
暫無資料
其他
暫無資料