Chinese
English
Postdoctoral Fellow  |  Tsai, Ming-Hsien  
 
contact
education
experience
interests
publications
 
 
 
 
 
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 299-309, 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 118-133, September 2014.
4. M.-H. Tsai, Y.-K. Tsay, and Y.-S. Hwang, "GOAL for games, omega-automata, and logics," Proceedings of the 25th International Conference on Computer Aided Verification (CAV), Lecture Notes in Computer Science, 8044, Springer, pages 883-889, 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 109-123, 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 261-271, 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 262-266, 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 assume-guarantee 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 643-657, October 2010.
9. Y.-F. Chen, E.M. Clarke, A. Farzan, M.-H. Tsai, Y.-K. Tsay, and B.-Y. Wang, "Automated assume-guarantee reasoning through implicit learning," Proceedings of the 22nd International Conference on Computer Aided Verification (CAV), Lecture Notes in Computer Science, 6174, Springer, pages 511-526, July 2010.
10. S. Magill, M.-H. Tsai, P. Lee, and Y.-K. Tsay, "Automatic numeric abstractions for heap-manipulating programs," Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), ACM, pages 211-222, 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 259-275, 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 428-432, 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 346--350, 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 466-471, 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 316-330, 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 105-119, December 2006.
 
 
bg