Ming-Hsien Tsai

Publication Activity (10 Years)

Years Active: 2006-2022
Publications (10 Years): 12

Top Topics

Recursive Programs

Algebraic Properties

Top Venues

IACR Trans. Cryptogr. Hardw. Embed. Syst.

Publications

Vincent Hwang, Jiaxiang Liu, Gregor Seiler, Xiaomu Shi, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang
Verified NTT Multiplications for NISTPQC KEM Lattice Finalists: Kyber, SABER, and NTRU. IACR Trans. Cryptogr. Hardw. Embed. Syst. 2022 (4) (2022)
Ming-Hsien Tsai, Yu-Fu Fu, Xiaomu Shi, Jiaxiang Liu, Bow-Yaw Wang, Bo-Yin Yang
Automatic Certified Verification of Cryptographic Programs with COQCRYPTOLINE. IACR Cryptol. ePrint Arch. 2022 (2022)
Xiaomu Shi, Yu-Fu Fu, Jiaxiang Liu, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang
CoqQFBV: A Scalable Certified SMT Quantifier-Free Bit-Vector Solver. CAV (2) (2021)
Yu-Fu Fu, Jiaxiang Liu, Xiaomu Shi, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang
Signed Cryptographic Program Verification with Typed CryptoLine. CCS (2019)
Yu-Fang Chen, Hsiao-chen Chung, Wen-Chi Hung, Ming-Hsien Tsai, Bow-Yaw Wang, Farn Wang
Synthesize Models for Quantitative Analysis Using Automata Learning. NETYS (2019)
Jiaxiang Liu, Xiaomu Shi, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang
Verifying Arithmetic in Cryptographic C Programs. ASE (2019)
Yu-Fang Chen, Matthias Heizmann, Ondrej Lengál, Yong Li, Ming-Hsien Tsai, Andrea Turrini, Lijun Zhang
Advanced automata-based algorithms for program termination checking. PLDI (2018)
Andy Polyakov, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang
Verifying Arithmetic Assembly Programs in Cryptographic Primitives (Invited Talk). CONCUR (2018)
Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang
Certified Verification of Algebraic Properties on Low-Level Mathematical Constructs in Cryptographic Programs. CCS (2017)
Ming-Hsien Tsai, Ming-Jium Shieh, Cheng-Liang Peng
A Targeting Self-breakable Agent for Increased Efficacy of Chemotherapeutic Drugs against Caco2 Cells. BIODEVICES (2016)
Frantisek Blahoudek, Matthias Heizmann, Sven Schewe, Jan Strejcek, Ming-Hsien Tsai
Complementing Semi-deterministic Büchi Automata. TACAS (2016)
Yu-Fang Chen, Chiao Hsieh, Ondrej Lengál, Tsung-Ju Lii, Ming-Hsien Tsai, Bow-Yaw Wang, Farn Wang
PAC learning-based verification and model synthesis. ICSE (2016)
Zuow-Zun Chen, Yen-Hsiang Wang, Jaewook Shin, Yan Zhao, Seyed Arash Mirhaj, Yen-Cheng Kuan, Huan-Neng Ron Chen, Chewnpu Jou, Ming-Hsien Tsai, Fu-Lung Hsueh, Mau-Chung Frank Chang
14.9 Sub-sampling all-digital fractional-N frequency synthesizer with -111dBc/Hz in-band phase noise and an FOM of -242dB. ISSCC (2015)
Yu-Fang Chen, Chiao Hsieh, Ming-Hsien Tsai, Bow-Yaw Wang, Farn Wang
CPArec: Verifying Recursive Programs via Source-to-Source Program Transformation - (Competition Contribution). TACAS (2015)
Yu-Fang Chen, Chiao Hsieh, Ondrej Lengál, Tsung-Ju Lii, Ming-Hsien Tsai, Bow-Yaw Wang, Farn Wang
PAC Learning-Based Verification and Model Synthesis. CoRR (2015)
Li-Wei Chu, Chun-Yu Lin, Ming-Dou Ker, Ming-Hsiang Song, Jeng-Chou Tseng, Chewnpu Jou, Ming-Hsien Tsai
ESD protection design for wideband RF applications in 65-nm CMOS process. ISCAS (2014)
Yu-Fang Chen, Chang-Hong Hsu, Hsin-Hung Lin, Peter Schwabe, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang, Shang-Yi Yang
Verifying Curve25519 Software. CCS (2014)
Yu-Fang Chen, Chiao Hsieh, Ming-Hsien Tsai, Bow-Yaw Wang, Farn Wang
Verifying Recursive Programs Using Intraprocedural Analyzers. SAS (2014)
Ming-Hsien Tsai, Seth Fogarty, Moshe Y. Vardi, Yih-Kuen Tsay
State of Büchi Complementation. Log. Methods Comput. Sci. 10 (4) (2014)
Yih-Kuen Tsay, Ming-Hsien Tsai, Jinn-Shu Chang, Yi-Wen Chang, Chi-Shiang Liu
Büchi Store: an open repository of $$\omega $$ -automata. Int. J. Softw. Tools Technol. Transf. 15 (2) (2013)
Ming-Hsien Tsai, Yih-Kuen Tsay, Yu-Shiang Hwang
GOAL for Games, Omega-Automata, and Logics. CAV (2013)
Li-Wei Chu, Chun-Yu Lin, Shiang-Yu Tsai, Ming-Dou Ker, Ming-Hsiang Song, Chewnpu Jou, Tse-Hua Lu, Jeng-Chou Tseng, Ming-Hsien Tsai, Tsun-Lai Hsu, Ping-Fang Hung, Tzu-Heng Chang
Compact and low-loss ESD protection design for V-band RF applications in a 65-nm CMOS technology. ISCAS (2012)
Kuanfu Chen, Ming-Hsien Tsai, Fu-Lung Hsueh, Wentai Liu
Analysis and design of data transmission protocol for 1024-channel retinal prosthesis. EMBC (2011)
Chun-Yu Lin, Li-Wei Chu, Shiang-Yu Tsai, Ming-Dou Ker, Tse-Hua Lu, Tsun-Lai Hsu, Ping-Fang Hung, Ming-Hsiang Song, Jeng-Chou Tseng, Tzu-Heng Chang, Ming-Hsien Tsai
Modified LC-tank ESD protection design for 60-GHz RF applications. ECCTD (2011)
Yih-Kuen Tsay, Ming-Hsien Tsai, Jinn-Shu Chang, Yi-Wen Chang
Büchi Store: An Open Repository of Büchi Automata. TACAS (2011)
Shawn S. H. Hsu, Ming-Hsien Tsai
Low-noise amplifiers with robust ESD protection for RF SOC. ISOCC (2011)
Yi-Kai Lo, Wentai Liu, Kuanfu Chen, Ming-Hsien Tsai, Fu-Lung Hsueh
A 64-channel neuron recording system. EMBC (2011)
Yu-Fang Chen, Edmund M. Clarke, Azadeh Farzan, Ming-Hsien Tsai, Yih-Kuen Tsay, Bow-Yaw Wang
Automated Assume-Guarantee Reasoning through Implicit Learning. CAV (2010)
Yu-Fang Chen, Edmund M. Clarke, Azadeh Farzan, Fei He, Ming-Hsien Tsai, Yih-Kuen Tsay, Bow-Yaw Wang, Lei Zhu
Comparing Learning Algorithms in Automated Assume-Guarantee Reasoning. ISoLA (1) (2010)
Hsieh-Hung Hsieh, Fu-Lung Hsueh, Chewnpu Jou, Fred Kuo, Sean Chen, Tzu-Jin Yeh, Kevin Kai-Wen Tan, Po-Yi Wu, Yu-Ling Lin, Ming-Hsien Tsai
A V-band divide-by-three differential direct injection-locked frequency divider in 65-nm CMOS. CICC (2010)
Ming-Hsien Tsai, Seth Fogarty, Moshe Y. Vardi, Yih-Kuen Tsay
State of Büchi Complementation. CIAA (2010)
Stephen Magill, Ming-Hsien Tsai, Peter Lee, Yih-Kuen Tsay
Automatic numeric abstractions for heap-manipulating programs. POPL (2010)
Yih-Kuen Tsay, Yu-Fang Chen, Ming-Hsien Tsai, Kang-Nien Wu, Wen-Chin Chan, Chi-Jian Luo, Jinn-Shu Chang
Tool support for learning Büchi automata and linear temporal logic. Formal Aspects Comput. 21 (3) (2009)
Yih-Kuen Tsay, Yu-Fang Chen, Ming-Hsien Tsai, Wen-Chin Chan, Chi-Jian Luo
GOAL Extended: Towards a Research Tool for Omega Automata and Temporal Logic. TACAS (2008)
Stephen Magill, Ming-Hsien Tsai, Peter Lee, Yih-Kuen Tsay
THOR: A Tool for Reasoning about Shape and Arithmetic. CAV (2008)
Yih-Kuen Tsay, Yu-Fang Chen, Ming-Hsien Tsai, Kang-Nien Wu, Wen-Chin Chan
GOAL: A Graphical Tool for Manipulating Büchi Automata and Temporal Formulae. TACAS (2007)
Ming-Hsien Tsai, Bow-Yaw Wang
Formalization of CTL* in Calculus of Inductive Constructions. ASIAN (2006)
Ming-Hsien Tsai, Bow-Yaw Wang
Modular Formalization of Reactive Modules in COQ. ASIAN (2006)