(Photograph by Wilson Tien)

TSAY, Yih-Kuen (蔡益坤) Professor Department of Information Management National Taiwan University (NTU) Mail: No. 1, Sec. 4, Roosevelt Rd., Taipei 106, TAIWAN Office: 1108, Management Building 2 Tel: (02) (or +8862) 3366 1189 Email: Xtsay@ntu.edu.twX (between the enclosing pair of X's)

This Web page describes my teaching duty and research effort as a faculty member in the Department of Information Management at NTU. If you have any questions or requests, please email me. By the way, here is My Public Map of the Web.

Last modified on September 2, 2024

Teaching

During a usual academic year, I teach the following courses (some seminars/projects excluded; click on the title for course info., notes, slides, old exams, etc.):

Algorithms (Fall)

Software Specification and Verification (Fall)

Theory of Computing (Spring)

Software Development Methods (Spring)

Note: I expect to be on sabbatical leave for the spring of 2025. Email me if you wish to know about the plan for a companion course to Software Specification and Verification that is offered sometimes: Automatic Verification.

---

Research

My research interests include Formal Verification, Temporal Logic, Automata Theory, Software Security, and the Semantic Web.

For the formal verification community, my group has developed a graphical interactive tool for omega-automata and temporal logic, called GOAL. It has a companion tool called Büchi Store, a Web-based open repository of ω-automata.

To know more about my research activities, please visit the website of my group SVVRL (Software Validation and Verification Research Laboratory).

Below is a list of my selected publications, among which the LICS 1996 paper won the 2016 LICS Test-of-Time Award. For links to the full text, please visit DBLP or Google Scholar.

(nothing beyond this publications list)

From Linear Temporal Logics to Büchi Automata: The Early and Simple Principle
Y.-K. Tsay and M.Y. Vardi
Model Checking, Synthesis, and Learning (Jonsson Festschrift), LNCS 13030, 8-40, 2021.

State of Büchi Complementation
M.-H. Tsai, S. Fogarty, M.Y. Vardi, and Y.-K. Tsay
Logical Methods in Computer Science, 2014. (arXiv:1406.4575)
A preliminary version appeared in The 15th International Conference on Implementation and Application of Automata (CIAA 2010), LNCS 6482, 261-271, 2011.

GOAL for Games, Omega-Automata, and Logics
M.-H. Tsai, Y.-K. Tsay, and Y.-S. Hwang
The 25th International Conference on Computer Aided Verification (CAV 2013), LNCS 8044, 883-889, July 2013.

Büchi Store: An Open Repository of ω-Automata
Y.-K. Tsay, M.-H. Tsai, J.-S. Chang, Y.-W. Chang, and C.-S. Liu
International Journal on Software Tools for Technology Transfer, 15(2):109-123, 2013.
(expanded from the TACAS 2011 version; available online: 10.1007/s10009-012-0268-4)

Automated Assume-Guarantee Reasoning through Implicit Learning
Y.-F. Chen, E.M. Clarke, A. Farzan, M.-H. Tsai, Y.-K. Tsay, and B.-Y. Wang
The 22nd International Conference on Computer Aided Verification (CAV 2010), LNCS 6174, 511-526, July 2010.

Automatic Numeric Abstractions for Heap-Manipulating Programs
S. Magill, M.-H. Tsai, P. Lee, and Y.-K. Tsay
The 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2010), 211-222, January 2010.

Automated Compositional Reasoning of Intuitionistically Closed Regular Properties
Y.-K. Tsay and B.-Y. Wang
International Journal of Foundations of Computer Science, 20(4):747-762, August 2009.

Tool Support for Learning Büchi Automata and Linear Temporal Logic
Y.-K. Tsay, Y.-F. Chen, M.-H. Tsai, K.-N. Wu, W.-C. Chan, C.-J. Luo, and J.-S. Chang
Formal Aspects of Computing, 21:259-275, 2009.

Learning Minimal Separating DFA's for Compositional Verification
Y.-F. Chen, A. Farzan, E.M. Clarke, Y.-K. Tsay, and B.-Y. Wang
The 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2009), LNCS 5505, 31-45, March 2009.

GOAL Extended: Towards a Research Tool for Omega Automata and Temporal Logic
Y.-K. Tsay, Y.-F. Chen, M.-H. Tsai, W.-C. Chan, and C.-J. Luo
The 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2008), LNCS 4963, 346--350, March/April 2008.

Extending Automated Compositional Verification to the Full Class of Omega-Regular Languages
A. Farzan, Y.-F. Chen, E.M. Clarke, Y.-K. Tsay, and B.-Y. Wang
The 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2008), LNCS 4963, 2--17, March/April 2008.

GOAL: A Graphical Tool for Manipulating Buechi Automata and Temporal Formulae
Y.-K. Tsay, Y.-F. Chen, M.-H. Tsai, K.-N. Wu, and W.-C. Chan
The 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2007), LNCS 4424, 466--471, March/April 2007.

Automated Technology for Verification and Analysis, Proceedings of ATVA 2005
D.A. Peled and Y.-K. Tsay (Eds.)
LNCS 3707. Springer, October 2005.

Algorithmic Analysis of Programs with Well Quasi-Ordered Domains
P.A. Abdulla, K. Cerans, B. Jonsson, and Y.-K. Tsay
Information and Computation, Vol. 160, No. 1/2, 109--127, August 2000.

Compositional Verification in Linear-Time Temporal Logic
Y.-K. Tsay
The Conference on Foundations of Software Science and Computation Structures (FOSSACS 2000), LNCS 1784, 344--358, March 2000.

Deriving a Scalable Algorithm for Mutual Exclusion
Y.-K. Tsay
The 12th International Symposium on Distributed Computing (DISC 1998), LNCS 1499, 393--407, September 1998.

Assumption/Guarantee Specifications in Linear-Time Temporal Logic
B. Jonsson and Y.-K. Tsay
Theoretical Computer Science, Vol. 167, 47--72, October 1996.
An extended abstract appeared in The 6th International Joint Conference on the Theory and Practice of Software Development (TAPSOFT) , LNCS 915, 262--276, May 1995.

General Decidability Theorems for Infinite-State Systems
P.A. Abdulla, K. Cerans, B. Jonsson, and Y.-K. Tsay
The 11th IEEE Symposium on Logic in Computer Science (LICS 1996), 313--321, July 1996.

Fault-Tolerant Algorithms for Fair Interprocess Synchronization
Y.-K. Tsay and R.L. Bagrodia
IEEE Transactions on Parallel and Distributed Systems, Vol. 5, No. 7, 737--748, 1994.

Some Impossibility Results in Interprocess Synchronization
Y.-K. Tsay and R.L. Bagrodia
Distributed Computing, 6(4):221--231, July 1993.