(Photograph by Wilson Tien)

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

This Web page describes my teaching duty and research effort in the Department of Information Management at National Taiwan University. If you have any questions or requests, please email me. By the way, here is My Map of the Web.

Last modified on April 13, 2009

Teaching

During Fall 2008 -- Spring 2009, I teach the following courses (seminars/projects excluded):

Software Development Methods (Fall 2008)

Software Specification and Verification (Fall 2008)

Information Security (Fall 2008) (by FTP only)

Algorithms (Spring 2009)

Automatic Verification (Spring 2009)

(Note: click on the title for course info., slides, old exams, etc.; the FTP site requires a guest account which is available upon request.)

---

Research

My research interests include Formal Verification, Temporal Logic and Automata, Software Security, and the Semantic Web. I am involved in the TWISC and the iCAST projects. And recently, my group has developed a graphical interactive tool for omega-automata and temporal logic, called GOAL. To know more about my research activities, please visit the Web site of my group SVVRL (Software Validation and Verification Research Laboratory).

Below is a list of my selected publications. Electronic copies are not provided due to copyright concerns. They should be easy to find with, e.g., DBLP or the Google Scholar (the publisher versions are usually better with citation information).

Tool Support for Learning Buechi 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. (DOI: 10.1007/s00165-008-0091-6)

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.

THOR: A Tool for Reasoning about Shape and Arithmetic
S. Magill, M.-H. Tsai, P. Lee, and Y.-K. Tsay
The 20th International Conference on Computer Aided Verification (CAV 2008), LNCS 5123, 428-432, July 2008.

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.

Composing Temporal-Logic Specifications with Machine Assistance
J.-W. Teng and Y.-K. Tsay
The 12th International Formal Methods Europe Symposium (FM 2003), LNCS 2805, September 2003.

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.