



Publications 

1. 
M.H. Tsai, S. Fogarty, M.Y. Vardi, and Y.K. Tsay, "State of Büchi Complementation," to appear in Logical Methods in Computer Science (LMCS). 
2. 
Y.F. Chen, C.H. Hsu, H.H. Lin, P. Schwabe, M.H. Tsai, B.Y. Wang, B.Y. Yang, and S.Y. Yang, "Verifying Curve25519 Software," Proceedings of the 21st ACM Conference on Computer and Communications Security (CCS), ACM, pages 299309, November 2014. 
3. 
Y.F. Chen, C. Hsieh, M.H. Tsai, B.Y. Wang, and F. Wang, "Verifying Recursive Programs using Intraprocedural Analyzers," Proceedings of the 21st International Static Analysis Symposium (SAS), Lecture Notes in Computer Science, 8723, Springer, pages 118133, September 2014. 
4. 
M.H. Tsai, Y.K. Tsay, and Y.S. Hwang, "GOAL for games, omegaautomata, and logics," Proceedings of the 25th International Conference on Computer Aided Verification (CAV), Lecture Notes in Computer Science, 8044, Springer, pages 883889, July 2013. 
5. 
Y.K. Tsay, M.H. Tsai, J.S. Chang, Y.W. Chang, and C.S. Liu, "Büchi Store: an open repository of ωautomata," International Journal on Software Tools for Technology Transfer (STTT), volume 15, number 2, pages 109123, February 2013. 
6. 
M.H. Tsai, S. Fogarty, M.Y. Vardi, and Y.K. Tsay, "State of Büchi complementation," Proceedings of the 15th International Conference on Implementation and Application of Automata (CIAA), Lecture Notes in Computer Science, 6482, Springer, pages 261271, August 2011. 
7. 
Y.K. Tsay, M.H. Tsai, J.S. Chang, and Y.W. Chang, "Büchi Store: An open repository of Büchi automata," Proceedings of the 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Lecture Notes in Computer Science, 6605, Springer, pages 262266, March 2011. 
8. 
Y.F. Chen, E.M. Clarke, A. Farzan, F. He, M.H. Tsai, Y.K. Tsay, B.Y. Wang, and L. Zhu, "Comparing learning algorithms in automated assumeguarantee reasoning," Proceedings of the 4th International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation (ISoLA), Lecture Notes in Computer Science, 6415, Springer, pages 643657, October 2010. 
9. 
Y.F. Chen, E.M. Clarke, A. Farzan, M.H. Tsai, Y.K. Tsay, and B.Y. Wang, "Automated assumeguarantee reasoning through implicit learning," Proceedings of the 22nd International Conference on Computer Aided Verification (CAV), Lecture Notes in Computer Science, 6174, Springer, pages 511526, July 2010. 
10. 
S. Magill, M.H. Tsai, P. Lee, and Y.K. Tsay, "Automatic numeric abstractions for heapmanipulating programs," Proceedings of the 37th ACM SIGPLANSIGACT Symposium on Principles of Programming Languages (POPL), ACM, pages 211222, January 2010. 
11. 
Y.K. Tsay, Y.F. Chen, M.H. Tsai, K.N. Wu, W.C. Chan, C.J. Luo, and J.S. Chang, "Tool support for learning Büchi automata and linear temporal logic," Formal Aspects of Computing, volume 21, number 3, pages 259275, February 2009. 
12. 
S. Magill, M.H. Tsai, P. Lee, and Y.K. Tsay, "THOR: A tool for reasoning about shape and arithmetic," Proceedings of the 20th International Conference on Computer Aided Verification (CAV), Lecture Notes in Computer Science, 5123, Springer, pages 428432, July 2008. 
13. 
Y.K. Tsay, Y.F. Chen, M.H. Tsai, W.C. Chan, and C.J. Luo, "GOAL Extended: Towards a Research Tool for Omega Automata and Temporal Logic," The 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2008), Lecture Notes in Computer Science, 4963, pages 346350, March 2008. 
14. 
Y.K. Tsay, Y.F. Chen, M.H. Tsai, K.N. Wu, and W.C. Chan, "GOAL: A graphical tool for manipulating Büchi automata and temporal formulae," Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Lecture Notes in Computer Science, 4424, Springer, pages 466471, March 2007. 
15. 
M.H. Tsai and B.Y. Wang, "Formalization of CTL* in Calculus of Inductive Constructions," Proceedings of the 11th Asian Computing Science Conference (ASIAN), Lecture Notes in Computer Science, 4435, Springer, pages 316330, December 2006. 
16. 
M.H. Tsai and B.Y. Wang, "Modular formalization of reactive modules in COQ," Proceedings of the 11th Asian Computing Science Conference (ASIAN), Lecture Notes in Computer Science, 4435, Springer, pages 105119, December 2006. 











