<title>Yih-Kuen Tsay @ NTUIM</title>

<H3> Yih-Kuen Tsay @ NTUIM </H3>

<P>
This Web page describes my <B>teaching duty</B> and
<B>research effort</B> in the Department of Information Management at
National Taiwan University, where I am an associate professor.

<P>
If you have any questions or requests, please send email to
<B>Xtsay@im.ntu.edu.twX</B> (remove the enclosing pair of X's).

<P>
BTW, here is <A HREF = "sites.html">My Map of the Web</A>.

<P>
<I>Last modified on April 18, 2008</I>

<HR>
<H2>Teaching</H2>
<P> During Fall 2007 -- Spring 2008, I will be teaching the following courses
(seminars/projects excluded):
<DL>
     <DT> <A HREF = "ftp://ftp.im.ntu.edu.tw/">Information Security</A> (Fall 2007)

<!--
     <DT> <A HREF = "http://joung.im.ntu.edu.tw/teaching/distributed_systems/2006/">
Distributed Information Systems</A> (Fall 2007)
-->
<!--
     <DT> <A HREF = "ftp://ftp.im.ntu.edu.tw/">Information Technology I</A>
-->
<!--
     <DT> <A HREF = "ftp://ftp.im.ntu.edu.tw/">E-Commerce Technologies</A>
 -->
<!--
     <DT> <A HREF = "ftp://ftp.im.ntu.edu.tw/">Software Development Methods</A> (Fall 2006)
 -->
     <DT> <A HREF = "ftp://ftp.im.ntu.edu.tw/">Software Specification and Verification</A> (Fall 2007)
<!--
     <DT> <A HREF = "ftp://ftp.im.ntu.edu.tw/">Software Project Management</A>
-->
     <DT> <A HREF = "ftp://ftp.im.ntu.edu.tw/">Algorithms</A> (Spring 2008)
     <DT> <A HREF = "ftp://ftp.im.ntu.edu.tw/">Automatic Verification</A> (Spring 2008)
<!--
     <DT> <A HREF = "ftp://ftp.im.ntu.edu.tw/">Theory of Computation</A>  (Spring 2008)
-->
<P> (Note: click on the title for course info., slides, old exams, etc.; most require a guest account
which is available upon request)

<!--
<P> The
     <A HREF = "ftp://ftp.im.ntu.edu.tw/">Theory of Computation</A>
     course is offered every two years; the next time will be Spring 2008.
-->
<!--
<P> The
     <A HREF = "ftp://ftp.im.ntu.edu.tw/">Software Project Management</A>
     course alternates with Software Development Methods; the next time will be Fall 2007.
-->

<!--
<P> If there is enough demand, I can also offer any of these elective
courses:
     <A HREF = "ftp://ftp.im.ntu.edu.tw/">Software Specification and Verification</A>
,
     <A HREF = "ftp://ftp.im.ntu.edu.tw/">Automatic Verification</A>
, and
     <A HREF = "ftp://ftp.im.ntu.edu.tw/">Distributed Algorithms</A>.
</DL>
-->

<HR>
<H2>Research</H2>
<P>
My research interests include Formal Verification, Distributed Algorithms/Systems,
Software Security, and the Semantic Web.
I am involved in the <A HREF = "http://www.icast.org.tw/">iCAST</A> project.
And recently, my group has developed a graphical interactive tool
for omega-automata and temporal logic, called <A HREF = "http://goal.im.ntu.edu.tw/">GOAL</A>.

<P>
Below is a list of my  <B>selected publications</B>.
Electronic copies are not provided due to copyright concerns;
they should be easy to find with, for example, the Google Scholar.

<P>
<DL>
     <DT>
     <B>GOAL Extended: Towards a Research Tool for Omega Automata and Temporal Logic</B> <BR>
     Y.-K. Tsay, Y.-F. Chen, M.-H. Tsai, W.-C. Chan, and C.-J. Luo <BR>
     <I>Proceedings of the 14th International Conference on Tools and Algorithms for the
     Construction and Analysis of Systems (TACAS 2008)</I>, LNCS 4963, 346--350,
     March/April 2008. <BR>
     <BR>
     
     <DT>
     <B>Extending Automated Compositional Verification to the Full Class of Omega-Regular 
     Languages</B> <BR>
     A. Farzan, Y.-F. Chen, E.M. Clarke, Y.-K. Tsay, and B.-Y. Wang <BR>
     <I>Proceedings of the 14th International Conference on Tools and Algorithms for the
     Construction and Analysis of Systems (TACAS 2008)</I>, LNCS 4963, 2--17,
     March/April 2008. <BR>
     <BR>

     <DT>
     <B>GOAL: A Graphical Tool for Manipulating Buchi Automata and Temporal Formulae</B> <BR>
     Y.-K. Tsay, Y.-F. Chen, M.-H. Tsai, K.-N. Wu, and W.-C. Chan <BR>
     <I>Proceedings of the 13th International Conference on Tools and Algorithms for the
     Construction and Analysis of Systems (TACAS 2007)</I>, LNCS 4424, 466--471,
     March/April 2007. <BR>
     <BR>

     <DT>
     <B>Tool Support for Learning Buchi Automata and Linear Temporal Logic</B> <BR>
     Y.-K. Tsay, Y.-F. Chen, and K.-N. Wu <BR>
     <I>The 2006 Formal Methodsin the Teaching Lab Workshop (A Workshop at the Formal
     Methods 2006 Symposium)</I>, Hamilton, Ontario, Canada, August 2006.  <BR>
     <BR>

     <DT>
     <I>Automated Technology for Verification and Analysis, Proceedings of ATVA 2005</I> <BR>
     D.A. Peled and Y.-K. Tsay (Eds.) <BR>
     LNCS 3707. Springer, October 2005. <BR>
     <BR>

     <DT>
     <B>Composing Temporal-Logic Specifications with Machine Assistance</B> <BR>
     J.-W. Teng and Y.-K. Tsay <BR>
     <I>Proceedings of the 12th International Formal Methods Europe
    Symposium (FM 2003)</I>, LNCS 2805, September 2003.  <BR>
     <BR>

     <DT>
     <B>Algorithmic Analysis of Programs with Well Quasi-Ordered Domains</B> <BR>
     P.A. Abdulla, K. Cerans, B. Jonsson, and Y.-K. Tsay <BR>
     <I> Information and Computation</I>, Vol. 160, No. 1/2, 109--127,
     August 2000.</I> <BR>
     <BR>

     <DT>
     <B>Compositional Verification in Linear-Time Temporal Logic</B> <BR>
     Y.-K. Tsay <BR>
     <I>Proceedings of the Conference on Foundations of Software Science and
     Computation Structures (FOSSACS 2000)</I>, LNCS 1784, 344--358, March 2000.  <BR>
     <BR>

     <DT>
     <B>Deriving a Scalable Algorithm for Mutual Exclusion</B> <BR>
     Y.-K. Tsay <BR>
     <I>Proceedings of the 12th International Symposium on Distributed
     Computing (DISC 1998)</I>, LNCS 1499, 393--407, September 1998.  <BR>
     <BR>

     <DT>
     <B>General Decidability Theorems for Infinite-State Systems</B> <BR>
     P.A. Abdulla, K. Cerans, B. Jonsson, and Y.-K. Tsay <BR>
     <I>Proceedings of the 11th IEEE Symposium on Logic
     in Computer Science (LICS 1996)</I>, 313--321, July 1996. <BR>
     <BR>

     <DT>
     <B>Assumption/Guarantee Specifications in Linear-Time Temporal
     Logic</B> <BR>
     B. Jonsson and Y.-K. Tsay <BR>
     <I> Theoretical Computer Science</I>, Vol. 167, 47--72, October
     1996.  <BR>
     An extended abstract appeared in
     <I> Proceedings of the 6th International Joint Conference on the
     Theory and Practice of Software Development (TAPSOFT)</I> , LNCS 915,
     262--276, May 1995. <BR>
     <BR>

     <DT>
     <B>Deducing Fairness Properties in UNITY Logic --- A New
     Completeness Result</B> <BR>
     Y.-K. Tsay and R.L. Bagrodia  <BR>
     <I>ACM Transactions on Programming Languages and Systems</I>, Vol. 17,
     No. 1, 16--27, January 1995.  <BR>
     <BR>

     <DT>
     <B>An Algorithm with Optimal Failure Locality for the Dining
     Philosophers Problem</B> <BR>
     Y.-K. Tsay and R.L. Bagrodia <BR>
     <I>Proceedings of the 8th International Workshop on Distributed
     Algorithms</I>, LNCS 857, 296--310, September 1994.  <BR>
     <BR>

     <DT>
     <B>Fault-Tolerant Algorithms for Fair Interprocess
     Synchronization</B> <BR>
     Y.-K. Tsay and R.L. Bagrodia <BR>
     <I>IEEE Transactions on Parallel and Distributed Systems</I>,
     Vol. 5, No. 7, 737--748, 1994.  <BR>
     <BR>
<!--
     <DT>
     <B>Operational Implication of Conditional UNITY
     Properties</B> <BR>
     Y.-K. Tsay and R.L. Bagrodia <BR>
     <I>Proceedings of DIMACS Workshop on Specification of
     Parallel Algorithms</I>, Princeton, New Jersey, May 1994.  <BR>
     <BR>
-->

     <DT>
     <B>Some Impossibility Results in Interprocess Synchronization</B> <BR>
     Y.-K. Tsay and R.L. Bagrodia <BR>
     <I>Distributed Computing</I>, 6(4):221--231, July 1993. <BR>
     <BR>
<!--
     <DT>
     <B>A Real-Time Algorithm for Fair Interprocess Synchronization</B> <BR>
     Y.-K. Tsay and R.L. Bagrodia <BR>
     <I>Proceedings of the 12th International Conference on
     Distributed Computing Systems (ICDCS)</I>, 716--723, June 1992. <BR>
     <BR>
-->

</DL>