Ming-Hsien Tsai

According to our database, Ming-Hsien Tsai authored at least 32 papers between 2006 and 2023.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of three.

2023

Automatic Verification of Cryptographic Block Function Implementations with Logical Equivalence Checking.

Li-Chang Lai, Jiaxiang Liu, Xiaomu Shi, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang

IACR Cryptol. ePrint Arch., 2023

llvm2CryptoLine: Verifying Arithmetic in Cryptographic C Programs.

Ruiling Chen, Jiaxiang Liu, Xiaomu Shi, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang

Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, 2023

CoqCryptoLine: A Verified Model Checker with Certified Results.

Ming-Hsien Tsai, Yu-Fu Fu, Jiaxiang Liu, Xiaomu Shi, Bow-Yaw Wang, Bo-Yin Yang

Proceedings of the Computer Aided Verification - 35th International Conference, 2023

Certified Verification for Algebraic Abstraction.

Ming-Hsien Tsai, Yu-Fu Fu, Jiaxiang Liu, Xiaomu Shi, Bow-Yaw Wang, Bo-Yin Yang

Proceedings of the Computer Aided Verification - 35th International Conference, 2023

2022

Verified NTT Multiplications for NISTPQC KEM Lattice Finalists: Kyber, SABER, and NTRU.

Vincent Hwang, Jiaxiang Liu, Gregor Seiler, Xiaomu Shi, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang

IACR Trans. Cryptogr. Hardw. Embed. Syst., 2022

Automatic Certified Verification of Cryptographic Programs with COQCRYPTOLINE.

Ming-Hsien Tsai, Yu-Fu Fu, Xiaomu Shi, Jiaxiang Liu, Bow-Yaw Wang, Bo-Yin Yang

IACR Cryptol. ePrint Arch., 2022

2021

CoqQFBV: A Scalable Certified SMT Quantifier-Free Bit-Vector Solver.

Xiaomu Shi, Yu-Fu Fu, Jiaxiang Liu, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang

Proceedings of the Computer Aided Verification - 33rd International Conference, 2021

2019

Synthesize Models for Quantitative Analysis Using Automata Learning.

Yu-Fang Chen, Hsiao-chen Chung, Wen-Chi Hung, Ming-Hsien Tsai, Bow-Yaw Wang, Farn Wang

Proceedings of the Networked Systems - 7th International Conference, 2019

Verifying Arithmetic in Cryptographic C Programs.

Jiaxiang Liu, Xiaomu Shi, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang

Proceedings of the 34th IEEE/ACM International Conference on Automated Software Engineering, 2019

Signed Cryptographic Program Verification with Typed CryptoLine.

Yu-Fu Fu, Jiaxiang Liu, Xiaomu Shi, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang

Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security, 2019

2018

Advanced automata-based algorithms for program termination checking.

Yu-Fang Chen, Matthias Heizmann, Ondrej Lengál, Yong Li, Ming-Hsien Tsai, Andrea Turrini, Lijun Zhang

Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2018

Verifying Arithmetic Assembly Programs in Cryptographic Primitives (Invited Talk).

Andy Polyakov, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang

Proceedings of the 29th International Conference on Concurrency Theory, 2018

2017

Certified Verification of Algebraic Properties on Low-Level Mathematical Constructs in Cryptographic Programs.

Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang

Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, 2017

2016

Complementing Semi-deterministic Büchi Automata.

Frantisek Blahoudek, Matthias Heizmann, Sven Schewe, Jan Strejcek, Ming-Hsien Tsai

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2016

PAC learning-based verification and model synthesis.

Yu-Fang Chen, Chiao Hsieh, Ondrej Lengál, Tsung-Ju Lii, Ming-Hsien Tsai, Bow-Yaw Wang, Farn Wang

Proceedings of the 38th International Conference on Software Engineering, 2016

A Targeting Self-breakable Agent for Increased Efficacy of Chemotherapeutic Drugs against Caco2 Cells.

Ming-Hsien Tsai, Ming-Jium Shieh, Cheng-Liang Peng

Proceedings of the 9th International Joint Conference on Biomedical Engineering Systems and Technologies (BIOSTEC 2016), 2016

2015

CPArec: Verifying Recursive Programs via Source-to-Source Program Transformation - (Competition Contribution).

Yu-Fang Chen, Chiao Hsieh, Ming-Hsien Tsai, Bow-Yaw Wang, Farn Wang

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2015

2014

State of Büchi Complementation.

Ming-Hsien Tsai, Seth Fogarty, Moshe Y. Vardi, Yih-Kuen Tsay

Log. Methods Comput. Sci., 2014

Verifying Recursive Programs Using Intraprocedural Analyzers.

Yu-Fang Chen, Chiao Hsieh, Ming-Hsien Tsai, Bow-Yaw Wang, Farn Wang

Proceedings of the Static Analysis - 21st International Symposium, 2014

Verifying Curve25519 Software.

Yu-Fang Chen, Chang-Hong Hsu, Hsin-Hung Lin, Peter Schwabe, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang, Shang-Yi Yang

Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, 2014

2013

Büchi Store: an open repository of ω-automata.

Yih-Kuen Tsay, Ming-Hsien Tsai, Jinn-Shu Chang, Yi-Wen Chang, Chi-Shiang Liu

Int. J. Softw. Tools Technol. Transf., 2013

GOAL for Games, Omega-Automata, and Logics.

Ming-Hsien Tsai, Yih-Kuen Tsay, Yu-Shiang Hwang

Proceedings of the Computer Aided Verification - 25th International Conference, 2013

2011

Büchi Store: An Open Repository of Büchi Automata.

Yih-Kuen Tsay, Ming-Hsien Tsai, Jinn-Shu Chang, Yi-Wen Chang

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2011

2010

Automatic numeric abstractions for heap-manipulating programs.

Stephen Magill, Ming-Hsien Tsai, Peter Lee, Yih-Kuen Tsay

Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2010

Comparing Learning Algorithms in Automated Assume-Guarantee Reasoning.

Yu-Fang Chen, Edmund M. Clarke, Azadeh Farzan, Fei He, Ming-Hsien Tsai, Yih-Kuen Tsay, Bow-Yaw Wang, Lei Zhu

Proceedings of the Leveraging Applications of Formal Methods, Verification, and Validation, 2010

Automated Assume-Guarantee Reasoning through Implicit Learning.

Yu-Fang Chen, Edmund M. Clarke, Azadeh Farzan, Ming-Hsien Tsai, Yih-Kuen Tsay, Bow-Yaw Wang

Proceedings of the Computer Aided Verification, 22nd International Conference, 2010

2009

Tool support for learning Büchi automata and linear temporal logic.

Yih-Kuen Tsay, Yu-Fang Chen, Ming-Hsien Tsai, Kang-Nien Wu, Wen-Chin Chan, Chi-Jian Luo, Jinn-Shu Chang

Formal Aspects Comput., 2009

2008

GOAL Extended: Towards a Research Tool for Omega Automata and Temporal Logic.

Yih-Kuen Tsay, Yu-Fang Chen, Ming-Hsien Tsai, Wen-Chin Chan, Chi-Jian Luo

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2008

THOR: A Tool for Reasoning about Shape and Arithmetic.

Stephen Magill, Ming-Hsien Tsai, Peter Lee, Yih-Kuen Tsay

Proceedings of the Computer Aided Verification, 20th International Conference, 2008

2007

GOAL: A Graphical Tool for Manipulating Büchi Automata and Temporal Formulae.

Yih-Kuen Tsay, Yu-Fang Chen, Ming-Hsien Tsai, Kang-Nien Wu, Wen-Chin Chan

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2007

2006

Formalization of CTL* in Calculus of Inductive Constructions.

Ming-Hsien Tsai, Bow-Yaw Wang

Proceedings of the Advances in Computer Science, 2006

Modular Formalization of Reactive Modules in COQ.

Ming-Hsien Tsai, Bow-Yaw Wang

Proceedings of the Advances in Computer Science, 2006