Yih-Kuen Tsay @ NTUIM
This Web page describes my teaching duty and
research effort in the Department of Information Management at
National Taiwan University, where I am an associate professor.
If you have any questions or requests, please send email to
Xtsay@im.ntu.edu.twX (remove the enclosing pair of X's).
BTW, here is My Map of the Web.
Last modified on April 18, 2008
Teaching
During Fall 2007 -- Spring 2008, I will be teaching the following courses
(seminars/projects excluded):
- Information Security (Fall 2007)
- Software Specification and Verification (Fall 2007)
- Algorithms (Spring 2008)
- Automatic Verification (Spring 2008)
(Note: click on the title for course info., slides, old exams, etc.; most require a guest account
which is available upon request)
Research
My research interests include Formal Verification, Distributed Algorithms/Systems,
Software Security, and the Semantic Web.
I am involved in the iCAST project.
And recently, my group has developed a graphical interactive tool
for omega-automata and temporal logic, called GOAL.
Below is a list of my selected publications.
Electronic copies are not provided due to copyright concerns;
they should be easy to find with, for example, the Google Scholar.
-
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
Proceedings of 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
Proceedings of 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 Buchi Automata and Temporal Formulae
Y.-K. Tsay, Y.-F. Chen, M.-H. Tsai, K.-N. Wu, and W.-C. Chan
Proceedings of the 13th International Conference on Tools and Algorithms for the
Construction and Analysis of Systems (TACAS 2007), LNCS 4424, 466--471,
March/April 2007.
-
Tool Support for Learning Buchi Automata and Linear Temporal Logic
Y.-K. Tsay, Y.-F. Chen, and K.-N. Wu
The 2006 Formal Methodsin the Teaching Lab Workshop (A Workshop at the Formal
Methods 2006 Symposium), Hamilton, Ontario, Canada, August 2006.
-
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
Proceedings of 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
Proceedings of 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
Proceedings of the 12th International Symposium on Distributed
Computing (DISC 1998), LNCS 1499, 393--407, September 1998.
-
General Decidability Theorems for Infinite-State Systems
P.A. Abdulla, K. Cerans, B. Jonsson, and Y.-K. Tsay
Proceedings of the 11th IEEE Symposium on Logic
in Computer Science (LICS 1996), 313--321, July 1996.
-
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
Proceedings of the 6th International Joint Conference on the
Theory and Practice of Software Development (TAPSOFT) , LNCS 915,
262--276, May 1995.
-
Deducing Fairness Properties in UNITY Logic --- A New
Completeness Result
Y.-K. Tsay and R.L. Bagrodia
ACM Transactions on Programming Languages and Systems, Vol. 17,
No. 1, 16--27, January 1995.
-
An Algorithm with Optimal Failure Locality for the Dining
Philosophers Problem
Y.-K. Tsay and R.L. Bagrodia
Proceedings of the 8th International Workshop on Distributed
Algorithms, LNCS 857, 296--310, September 1994.
-
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.