This is an old revision of the document!
Publications
(Note: this publications list also inlcudes papers that were published during earlier incarations of this laboratory. Please visit DBLP for links to the publisher's electronic version of full text.)
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)
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.
Büchi Store: An Open Repository of Büchi Automata
Y.-K. Tsay, M.-H. Tsai, J.-S. Chang, and Y.-W. Chang
The 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2011), LNCS 6605, 262-266, March-April 2011.
State of Büchi Complementation
M.-H. Tsai, S. Fogarty, M.Y. Vardi, and Y.-K. Tsay
The 15th International Conference on Implementation and Application of Automata (CIAA 2010), LNCS 6482, 261-271, 2011.
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.
Tool Support for Learning Buchi 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(3):259-275, 2009. (DOI: 10.1007/s00165-008-0091-6)
Note: this is a revised and extended version of the one presented at the 2006 Formal Methods in the Teaching Lab Workshop, August 2006.
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.
Automated Compositional Reasoning of Intuitionistically Closed Regular Properties
Y.-K. Tsay and B.-Y. Wang
in Proceedings of the 13th International Conference on Implementation and Application of Automata (CIAA 2008), LNCS 5148, 36-45, Springer. [NSC96-3114-P-001-002-Y], 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 Buchi 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 (ATVA 2005) – Preface
D.A. Peled and Y.-K. Tsay
International Journal of Foundations of Computer Science, Vol. 18, No. 1, 1-3. (Note: preface to the ATVA 2005 Special Issue), February 2007.
Modular Formalization of Reactive Modules in COQ
Ming-Hsien Tsai, Bow-Yaw Wang
ASIAN 2006: 105-119
Formalization of CTL* in Calculus of Inductive Constructions
Ming-Hsien Tsai, Bow-Yaw Wang
ASIAN 2006: 316-330
Tool Support for Learning Büchi Automata and Linear Temporal Logic
Y.-K. Tsay, Y.-F. Chen, and K.-N. Wu
The 2006 Formal Methods in the Teaching Lab Workshop(A Workshop at the Formal Methods 2006 Symposium), McMaster University, 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
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.
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.
