跳到主要內容區
:::
  1. 首頁
  2. 全系師資

蔡明憲　Ming-Hsien Tsai

Ming-Hsien Tsai
Ming-Hsien Tsai

職稱

  • 助理教授

 

專長及研究領域

  • 正規方法、程式驗證、時態邏輯、自動機、模型檢驗、定理證明

 

教授課程

  • 軟體安全（研究所）
  • 決策程序與密碼驗證應用（研究所）

 

聯絡方式
  • 辦公室：IA-906
  • 電　話：(02)2730-3794
  • 信　箱：mhtsai@cs.ntust.edu.tw

 

實驗室
  • 軟體安全實驗室

 

學歷
  • 2013 國立臺灣大學資訊管理研究所 博士
  • 2004 國立臺灣大學資訊管理研究所 碩士
  • 2002 國立臺灣大學會計系、資訊管理系 學士

 

經歷

  • 2023 國家資通安全研究院 副研究員
  • 2021-2023 國家實驗研究院 副研究員
  • 2018 國立臺灣大學 資訊管理系 兼任助理教授
  • 2018 國立臺灣師範大學 資訊工程學系 兼任助理教授
  • 2013-2021 中央研究院 博士後研究員

 

期刊論文

  • V. Hwang, J. Liu, G. Seiler, X. Shi, M.-H. Tsai, B.-Y. Wang, and B.-Y. Yang. Verified NTT Multiplications for NISTPQC KEM Lattice Finalists: Kyber, SABER, and NTRU. In IACR Transactions on Cryptographic Hardware and Embedded Systems, 2022(4): 718–750, 2022.
  • M.-H. Tsai, S. Fogarty, M.Y. Vardi, and Y.-K. Tsay. State of Büchi Complementation. Logical Methods in Computer Science (LMCS), 10(4), 2014.
  • 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), 15(2): 109–123, February 2013.
  • 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, 21(3):259-275, February 2009.

 

研討會論文

  • R. Chen, J. Liu, X. Shi, M.-H. Tsai, B.-Y. Wang, and B.-Y. Yang. llvm2CryptoLine: Verifying Arithmetic in Cryptographic C Programs. In Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE), 2023. To appear.
  • M.-H. Tsai, Y.-F. Fu, J. Liu, X. Shi, B.-Y. Wang, and B.-Y. Yang. Certified Verification for Algebraic Abstraction. In Proceedings of the 35th International Conference on Computer Aided Verification (CAV) Part III, LNCS 13966, pages 329–349, 2023.
  • M.-H. Tsai, Y.-F. Fu, J. Liu, X. Shi, B.-Y. Wang, and B.-Y. Yang. CoqCryptoLine: A Verified Model Checker with Certified Results. In Proceedings of the 35th International Conference on Computer Aided Verification (CAV) Part II, LNCS 13965, pages 227–240, 2023.
  • M.-H. Tsai, Y.-F. Fu, X. Shi, J. Liu, B.-Y. Wang, B.-Y. Yang. Automatic Certified Verification of Cryptographic Programs with CoqCryptoLine. In IACR Cryptology ePrint Archive, 2022:1116, 2022.
  • X. Shi, Y.-F. Fu, J. Liu, M.-H. Tsai, B.-Y. Wang, and B.-Y. Yang. CoqQFBV: A Scalable Certified SMT Quantifier-Free Bit-Vector Solver. In Proceedings of the 33rd International Conference on Computer Aided Verification (CAV) Part II, LNCS 12760, pages 149–171, Springer, 2021.
  • J. Liu, X. Shi, M.-H. Tsai, B.-Y. Wang, and B.-Y. Yang. Verifying Arithmetic in Cryptographic C Programs. In Proceedings of the 34th IEEE/ACM International Conference on Automated Software Engineering (ASE), pages 552–564, IEEE, 2019.
  • Y.-F. Fu, J. Liu, X. Shi, M.-H. Tsai, B.-Y. Wang, and B.-Y. Yang. Signed Cryptographic Program Verification with Typed CryptoLine. In Proceedings of the 26th ACM Conference on Computer and Communications Security (CCS), pages 1591–1606, ACM, November 2019.
  • Y.-F. Chen, H.-C. Chung, W.-C. Hung, M.-H. Tsai, B.-Y. Wang, and F. Wang. Synthesize Models for Quantitative Analysis Using Automata Learning. In Proceedings of the 7th International Conference on Networked Systems (NETYS), pages 75–92, Springer, 2019.
  • A. Polyakov, M.-H. Tsai, B.-Y. Wang, and B.-Y. Yang: Verifying Arithmetic Assembly Programs in Cryptographic Primitives (Invited Talk). In Proceedings of the 29th International Conference on Concurrency Theory (CONCUR), pages 4:1–4:16, LIPIcs 118, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018.
  • Y.-F. Chen, M. Heizmann, O. Lengál, Y. Li, M.-H. Tsai, A. Turrini, and L. Zhang. Advanced Automata-Based Algorithms for Program Termination Checking. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 135–150, ACM, June 2018.
  • M.-H. Tsai, B.-Y. Wang, and B.-Y. Yang. Certified Verification of Algebraic Properties on Low-Level Mathematical Constructs in Cryptographic Programs. In Proceedings of the 24th ACM Conference on Computer and Communications Security (CCS), pages 1973– 1987, ACM, October/November 2017.
  • Y.-F. Chen, C. Hsieh, O. Lengál, T.-J. Lii, M.-H. Tsai, B.-Y. Wang, and F. Wang. PAC learning-based verification and model synthesis. In Proceedings of the 38th International Conference on Software Engineering (ICSE), pages 714–724. ACM, May 2016.
  • F. Blahoudek, M. Heizmann, S. Schewe, J. Strejček, and M.-H. Tsai. Complementing semi-deterministic Büchi automata. In Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS 9636, pages 770–787. Springer, April 2016.
  • Y.-F. Chen, C. Hsieh, M.-H. Tsai, B.-Y. Wang, and F. Wang. CPArec: Verifying recursive programs via source-to-source program transformation - (competition contribution). In Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS 9035, pages 426–428. Springer, April 2015.
  • 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. In Proceedings of the 21st ACM Conference on Computer and Communications Security (CCS), pages 299–309. ACM, November 2014.
  • Y.-F. Chen, C. Hsieh, M.-H. Tsai, B.-Y. Wang, and F. Wang. Verifying recursive programs using intraprocedural analyzers. In Proceedings of the 21st International Static Analysis Symposium (SAS), LNCS 8723, pages 118–133. Springer, September 2014.
  • M.-H. Tsai, Y.-K. Tsay, and Y.-S. Hwang. GOAL for games, omega-automata, and logics. In Proceedings of the 25th International Conference on Computer Aided Verification (CAV), LNCS 8044, pages 883–889. Springer, July 2013.
  • Y.-K. Tsay, M.-H. Tsai, J.-S. Chang, and Y.-W. Chang. Büchi Store: An open repository of Büchi automata. In Proceedings of the 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS 6605, pages 262–266. Springer, March/April 2011.
  • 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. In Proceedings of the 22nd International Conference on Computer Aided Verification (CAV), LNCS 6174, pages 511–526. Springer, July 2010.
  • 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. In Proceedings of the 4th International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation (ISoLA), LNCS 6415, pages 643–657. Springer, October 2010.
  • S. Magill, M.-H. Tsai, P. Lee, and Y.-K. Tsay. Automatic numeric abstractions for heap-manipulating programs. In Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 211–222. ACM, January 2010.
  • M.-H. Tsai, S. Fogarty, M.Y. Vardi, and Y.-K. Tsay. State of Büchi complementation. In Proceedings of the 15th International Conference on Implementation and Application of Automata (CIAA), LNCS 6482, pages 261–271. Springer, August 2011.
  • S. Magill, M.-H. Tsai, P. Lee, and Y.-K. Tsay. THOR: A tool for reasoning about shape and arithmetic. In Proceedings of the 20th International Conference on Computer Aided Verification (CAV), LNCS 5123, pages 428-432. Springer, July 2008.
  • 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. In Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS 4963, pages 346–350. Springer, March/April 2008.
  • 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. In Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS 4424, pages 466–471. Springer, March/April 2007.
  • M.-H. Tsai and B.-Y. Wang. Modular formalization of reactive modules in COQ. In Proceedings of the 11th Asian Computing Science Conference (ASIAN), LNCS 4435, pages 105–119. Springer, December 2006.
  • M.-H. Tsai, B.-Y. Wang. Formalization of CTL* in Calculus of Inductive Constructions. In Proceedings of the 11th Asian Computing Science Conference (ASIAN), LNCS 4435, pages 316–330. Springer, December 2006.

  

 

瀏覽數: