A Real-Time Algorithm for Fair Interprocess Synchronization. - Yih-Kuen Tsay; Rajive L. Bagrodia (ICDCS, 1992)

Some Impossibility Results in Interprocess Synchronization. - Yih-Kuen Tsay; Rajive L. Bagrodia (Distributed Comput., 1993)

Operational Implication of Conditional Unity Properties. - Yih-Kuen Tsay; Rajive L. Bagrodia (Specification of Parallel Algorithms, 1994)

An Algorithm with Optimal Failure Locality for the Dining Philosophers Problem. - Yih-Kuen Tsay; Rajive L. Bagrodia (WDAG, 1994)

Fault-Tolerant Algorithms for Fair Interprocess Synchronization. - Yih-Kuen Tsay; Rajive L. Bagrodia (IEEE Trans. Parallel Distributed Syst., 1994)

Assumption/Guarantee Specifications in Linear-Time Temporal Logic (Extended Abstract). - Bengt Jonsson 001; Yih-Kuen Tsay (TAPSOFT, 1995)

Deducing Fairness Properties in UNITY Logic - A New Completeness Result. - Yih-Kuen Tsay; Rajive L. Bagrodia (ACM Trans. Program. Lang. Syst., 1995)

General Decidability Theorems for Infinite-State Systems. - Parosh Aziz Abdulla; Karlis Cerans; Bengt Jonsson 001; Yih-Kuen Tsay (LICS, 1996)

Assumption/Guarantee Specifications in Linear-Time Temporal Logic. - Bengt Jonsson 001; Yih-Kuen Tsay (Theor. Comput. Sci., 1996)

Deriving a Scalable Algorithm for Mutual Exclusion. - Yih-Kuen Tsay (DISC, 1998)

Compositional Verification in Linear-Time Temporal Logic. - Yih-Kuen Tsay (FoSSaCS, 2000)

Algorithmic Analysis of Programs with Well Quasi-ordered Domains. - Parosh Aziz Abdulla; Karlis Cerans; Bengt Jonsson 001; Yih-Kuen Tsay (Inf. Comput., 2000)

Composing Temporal-Logic Specifications with Machine Assistance. - Jei-Wen Teng; Yih-Kuen Tsay (FME, 2003)

GOAL: A Graphical Tool for Manipulating Büchi Automata and Temporal Formulae. - Yih-Kuen Tsay; Yu-Fang Chen 001; Ming-Hsien Tsai 001; Kang-Nien Wu; Wen-Chin Chan (TACAS, 2007)

Preface. - Doron A. Peled; Yih-Kuen Tsay (Int. J. Found. Comput. Sci., 2007)

THOR: A Tool for Reasoning about Shape and Arithmetic. - Stephen Magill; Ming-Hsien Tsai 001; Peter Lee 001; Yih-Kuen Tsay (CAV, 2008)

Extending Automated Compositional Verification to the Full Class of Omega-Regular Languages. - Azadeh Farzan; Yu-Fang Chen 001; Edmund M. Clarke; Yih-Kuen Tsay; Bow-Yaw Wang (TACAS, 2008)

GOAL Extended: Towards a Research Tool for Omega Automata and Temporal Logic. - Yih-Kuen Tsay; Yu-Fang Chen 001; Ming-Hsien Tsai 001; Wen-Chin Chan; Chi-Jian Luo (TACAS, 2008)

Learning Minimal Separating DFA's for Compositional Verification. - Yu-Fang Chen 001; Azadeh Farzan; Edmund M. Clarke; Yih-Kuen Tsay; Bow-Yaw Wang (TACAS, 2009)

Tool support for learning Büchi automata and linear temporal logic. - Yih-Kuen Tsay; Yu-Fang Chen 001; Ming-Hsien Tsai 001; Kang-Nien Wu; Wen-Chin Chan; Chi-Jian Luo; Jinn-Shu Chang (Formal Aspects Comput., 2009)

Automated Compositional Reasoning of Intuitionistically Closed Regular Properties. - Yih-Kuen Tsay; Bow-Yaw Wang (Int. J. Found. Comput. Sci., 2009)

Automated Assume-Guarantee Reasoning through Implicit Learning. - Yu-Fang Chen 001; Edmund M. Clarke; Azadeh Farzan; Ming-Hsien Tsai 001; Yih-Kuen Tsay; Bow-Yaw Wang (CAV, 2010)

Comparing Learning Algorithms in Automated Assume-Guarantee Reasoning. - Yu-Fang Chen 001; Edmund M. Clarke; Azadeh Farzan; Fei He 001; Ming-Hsien Tsai 001; Yih-Kuen Tsay; Bow-Yaw Wang; Lei Zhu (ISoLA (1), 2010)

Automatic numeric abstractions for heap-manipulating programs. - Stephen Magill; Ming-Hsien Tsai 001; Peter Lee 001; Yih-Kuen Tsay (POPL, 2010)

Büchi Store: An Open Repository of Büchi Automata. - Yih-Kuen Tsay; Ming-Hsien Tsai 001; Jinn-Shu Chang; Yi-Wen Chang (TACAS, 2011)

GOAL for Games, Omega-Automata, and Logics. - Ming-Hsien Tsai 001; Yih-Kuen Tsay; Yu-Shiang Hwang (CAV, 2013)

Büchi Store: an open repository of ω-automata. - Yih-Kuen Tsay; Ming-Hsien Tsai 001; Jinn-Shu Chang; Yi-Wen Chang; Chi-Shiang Liu (Int. J. Softw. Tools Technol. Transf., 2013)

State of Büchi Complementation. - Ming-Hsien Tsai 001; Seth Fogarty; Moshe Y. Vardi; Yih-Kuen Tsay (Log. Methods Comput. Sci., 2014)

From Linear Temporal Logics to Büchi Automata: The Early and Simple Principle. - Yih-Kuen Tsay; Moshe Y. Vardi (Model Checking, Synthesis, and Learning, 2021)

Congruence Relations for Büchi Automata. - Yong Li 031; Yih-Kuen Tsay; Andrea Turrini; Moshe Y. Vardi; Lijun Zhang 001 (FM, 2021)

Congruence Relations for Büchi Automata. - Yong Li 031; Yih-Kuen Tsay; Moshe Y. Vardi (CoRR, 2021)

Towards a Grand Unification of Büchi Complementation Constructions. - Moshe Y. Vardi; Seth Fogarty; Yong Li 031; Yih-Kuen Tsay (Principles of Systems Design, 2022)