Modular Formalization of Reactive Modules in COQ. - Ming-Hsien Tsai 001; Bow-Yaw Wang (ASIAN, 2006)

Formalization of CTL* in Calculus of Inductive Constructions. - Ming-Hsien Tsai 001; Bow-Yaw Wang (ASIAN, 2006)

GOAL: A Graphical Tool for Manipulating Büchi Automata and Temporal Formulae. - Yih-Kuen Tsay; Yu-Fang Chen 001; Ming-Hsien Tsai 001; Kang-Nien Wu; Wen-Chin Chan (TACAS, 2007)

THOR: A Tool for Reasoning about Shape and Arithmetic. - Stephen Magill; Ming-Hsien Tsai 001; Peter Lee 001; Yih-Kuen Tsay (CAV, 2008)

GOAL Extended: Towards a Research Tool for Omega Automata and Temporal Logic. - Yih-Kuen Tsay; Yu-Fang Chen 001; Ming-Hsien Tsai 001; Wen-Chin Chan; Chi-Jian Luo (TACAS, 2008)

Tool support for learning Büchi automata and linear temporal logic. - Yih-Kuen Tsay; Yu-Fang Chen 001; Ming-Hsien Tsai 001; Kang-Nien Wu; Wen-Chin Chan; Chi-Jian Luo; Jinn-Shu Chang (Formal Aspects Comput., 2009)

Automated Assume-Guarantee Reasoning through Implicit Learning. - Yu-Fang Chen 001; Edmund M. Clarke; Azadeh Farzan; Ming-Hsien Tsai 001; Yih-Kuen Tsay; Bow-Yaw Wang (CAV, 2010)

Comparing Learning Algorithms in Automated Assume-Guarantee Reasoning. - Yu-Fang Chen 001; Edmund M. Clarke; Azadeh Farzan; Fei He 001; Ming-Hsien Tsai 001; Yih-Kuen Tsay; Bow-Yaw Wang; Lei Zhu (ISoLA (1), 2010)

Automatic numeric abstractions for heap-manipulating programs. - Stephen Magill; Ming-Hsien Tsai 001; Peter Lee 001; Yih-Kuen Tsay (POPL, 2010)

Büchi Store: An Open Repository of Büchi Automata. - Yih-Kuen Tsay; Ming-Hsien Tsai 001; Jinn-Shu Chang; Yi-Wen Chang (TACAS, 2011)

GOAL for Games, Omega-Automata, and Logics. - Ming-Hsien Tsai 001; Yih-Kuen Tsay; Yu-Shiang Hwang (CAV, 2013)

Büchi Store: an open repository of ω-automata. - Yih-Kuen Tsay; Ming-Hsien Tsai 001; Jinn-Shu Chang; Yi-Wen Chang; Chi-Shiang Liu (Int. J. Softw. Tools Technol. Transf., 2013)

Verifying Curve25519 Software. - Yu-Fang Chen 001; Chang-Hong Hsu; Hsin-Hung Lin; Peter Schwabe; Ming-Hsien Tsai 001; Bow-Yaw Wang; Bo-Yin Yang; Shang-Yi Yang (CCS, 2014)

Verifying Recursive Programs Using Intraprocedural Analyzers. - Yu-Fang Chen 001; Chiao Hsieh; Ming-Hsien Tsai 001; Bow-Yaw Wang; Farn Wang (SAS, 2014)

State of Büchi Complementation. - Ming-Hsien Tsai 001; Seth Fogarty; Moshe Y. Vardi; Yih-Kuen Tsay (Log. Methods Comput. Sci., 2014)

CPArec: Verifying Recursive Programs via Source-to-Source Program Transformation - (Competition Contribution). - Yu-Fang Chen 001; Chiao Hsieh; Ming-Hsien Tsai 001; Bow-Yaw Wang; Farn Wang (TACAS, 2015)

A Targeting Self-breakable Agent for Increased Efficacy of Chemotherapeutic Drugs against Caco2 Cells. - Ming-Hsien Tsai 001; Ming-Jium Shieh; Cheng-Liang Peng (BIODEVICES, 2016)

PAC learning-based verification and model synthesis. - Yu-Fang Chen 001; Chiao Hsieh; Ondrej Lengál; Tsung-Ju Lii; Ming-Hsien Tsai 001; Bow-Yaw Wang; Farn Wang (ICSE, 2016)

Complementing Semi-deterministic Büchi Automata. - Frantisek Blahoudek; Matthias Heizmann; Sven Schewe; Jan Strejcek; Ming-Hsien Tsai 001 (TACAS, 2016)

Certified Verification of Algebraic Properties on Low-Level Mathematical Constructs in Cryptographic Programs. - Ming-Hsien Tsai 001; Bow-Yaw Wang; Bo-Yin Yang (CCS, 2017)

Verifying Arithmetic Assembly Programs in Cryptographic Primitives (Invited Talk). - Andy Polyakov; Ming-Hsien Tsai 001; Bow-Yaw Wang; Bo-Yin Yang (CONCUR, 2018)

Advanced automata-based algorithms for program termination checking. - Yu-Fang Chen 001; Matthias Heizmann; Ondrej Lengál; Yong Li 031; Ming-Hsien Tsai 001; Andrea Turrini; Lijun Zhang 001 (PLDI, 2018)

Signed Cryptographic Program Verification with Typed CryptoLine. - Yu-Fu Fu; Jiaxiang Liu 001; Xiaomu Shi; Ming-Hsien Tsai 001; Bow-Yaw Wang; Bo-Yin Yang (CCS, 2019)

Verifying Arithmetic in Cryptographic C Programs. - Jiaxiang Liu 001; Xiaomu Shi; Ming-Hsien Tsai 001; Bow-Yaw Wang; Bo-Yin Yang (ASE, 2019)

Synthesize Models for Quantitative Analysis Using Automata Learning. - Yu-Fang Chen 001; Hsiao-chen Chung; Wen-Chi Hung; Ming-Hsien Tsai 001; Bow-Yaw Wang; Farn Wang (NETYS, 2019)

CoqQFBV: A Scalable Certified SMT Quantifier-Free Bit-Vector Solver. - Xiaomu Shi; Yu-Fu Fu; Jiaxiang Liu 001; Ming-Hsien Tsai 001; Bow-Yaw Wang; Bo-Yin Yang (CAV (2), 2021)

Automatic Certified Verification of Cryptographic Programs with COQCRYPTOLINE. - Ming-Hsien Tsai 001; Yu-Fu Fu; Xiaomu Shi; Jiaxiang Liu 001; Bow-Yaw Wang; Bo-Yin Yang (IACR Cryptol. ePrint Arch., 2022)

Verified NTT Multiplications for NISTPQC KEM Lattice Finalists: Kyber, SABER, and NTRU. - Vincent Hwang; Jiaxiang Liu 001; Gregor Seiler; Xiaomu Shi; Ming-Hsien Tsai 001; Bow-Yaw Wang; Bo-Yin Yang (IACR Trans. Cryptogr. Hardw. Embed. Syst., 2022)

Certified Verification for Algebraic Abstraction. - Ming-Hsien Tsai 001; Yu-Fu Fu; Jiaxiang Liu 001; Xiaomu Shi; Bow-Yaw Wang; Bo-Yin Yang (CAV (3), 2023)

CoqCryptoLine: A Verified Model Checker with Certified Results. - Ming-Hsien Tsai 001; Yu-Fu Fu; Jiaxiang Liu 001; Xiaomu Shi; Bow-Yaw Wang; Bo-Yin Yang (CAV (2), 2023)

llvm2CryptoLine: Verifying Arithmetic in Cryptographic C Programs. - Ruiling Chen; Jiaxiang Liu 001; Xiaomu Shi; Ming-Hsien Tsai 001; Bow-Yaw Wang; Bo-Yin Yang (ESEC/SIGSOFT FSE, 2023)

Automatic Verification of Cryptographic Block Function Implementations with Logical Equivalence Checking. - Li-Chang Lai; Jiaxiang Liu 001; Xiaomu Shi; Ming-Hsien Tsai 001; Bow-Yaw Wang; Bo-Yin Yang (IACR Cryptol. ePrint Arch., 2023)

Algebraic Linear Analysis for Number Theoretic Transform in Lattice-Based Cryptography. - Chun-Ming Chiu; Jiaxiang Liu 001; Ming-Hsien Tsai 001; Xiaomu Shi; Bow-Yaw Wang; Bo-Yin Yang (IACR Trans. Cryptogr. Hardw. Embed. Syst., 2025)