LICS Test-of-Time Award (General Decidability Theorems for Infinite-State Systems, 1996)
經歷
2010/08 – Present
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
研討會論文
Yong Li, Yih-Kuen Tsay, Andrea Turrini, Moshe Y. Vardi, Lijun Zhang, 2021, Congruence Relations for Büchi Automata, Formal Methods (FM21), (Beijing, China).
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).
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).
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).
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).
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).
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).
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).
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).
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).
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).
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).
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).
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).
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).
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).
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).
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).
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).
蔡益坤、饒訓豪、劉智雄, July 2003, 以知識本體為基礎的網路服務媒合方法, 第十四屆國際資訊管理研討會, (Chiayi, Taiwan).
蔡益坤、王佳竣、陳柏均, July 2003, 網路服務撮合系統之設計與實作 － 以旅程計畫為例, 第十四屆國際資訊管理研討會, (Chiayi, Taiwan).
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).
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.
Y. -K. Tsay, September 1998, Deriving a Scalable Algorithm for Mutual Exclusion, Proceedings of the 12th International Symposium on Distributed Computing (DISC, formerly WDAG).
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).
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).
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).
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).
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).
期刊論文
Moshe Y. Vardi, Seth Fogarty, Yong Li, Yih-Kuen Tsay, 2022, Towards a Grand Unification of Büchi Complementation Constructions, Principles of Systems Design, LNCS,volume 13660 ,pp 185–207.
Y.-K. Tsay and M.Y. Vardi, 2021, From Linear Temporal Logics to Büchi Automata: The Early and Simple Principle, Model Checking, Synthesis, and Learning (Jonsson Festschrift), LNTCS,volume 13030 , 8-40.
M.-H. Tsai, S. Fogarty, M.Y. Vardi, and Y.-K. Tsay, January 2014, State of Büchi Complementation, Logical Methods in Computer Science, Volume 10, Issue 4.
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.
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.
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.
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.
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.
B. Jonsson, Y. -K. Tsay, October 1996, Assumption/Guarantee Specifications in Linear-Time Temporal Logic, Theoretical Computer Science, 47 - 72.
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.
Y. -K. Tsay, R. L. Bagrodia, July 1994, Fault-Tolerant Algorithms for Fair Interprocess Synchronization, IEEE Transactions on Parallel and Distributed Systems, 737 - 748.
Y. -K. Tsay, R. L. Bagrodia, July 1993, Some Impossibility Results in Interprocess Synchronization, Distributed Computing, 221 - 231.
