Ming-Hsien Tsai

37 papers A* 11A 5B 2C 1Journal 8Unranked 10
YearRankTypeTitle / Venue / Authors
2025 J jnl
Algebraic Linear Analysis for Number Theoretic Transform in Lattice-Based Cryptography.
IACR Trans. Cryptogr. Hardw. Embed. Syst.
Chun-Ming Chiu, Jiaxiang Liu, Ming-Hsien Tsai, Xiaomu Shi, Bow-Yaw Wang, Bo-Yin Yang
2025 A* conf
Jazzline: Composable CryptoLine Functional Correctness Proofs for Jasmin Programs.
CCS
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Lionel Blatter, Gustavo Xavier Delerue Marinho Alves, João Diogo Duarte, Benjamin Grégoire, Tiago Oliveira, Miguel Quaresma, Pierre-Yves Strub, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang
2024 — conf
Automatic Verification of Cryptographic Block Function Implementations with Logical Equivalence Checking.
ESORICS (4)
Li-Chang Lai, Jiaxiang Liu, Xiaomu Shi, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang
2023 J jnl
Automatic Verification of Cryptographic Block Function Implementations with Logical Equivalence Checking.
IACR Cryptol. ePrint Arch.
Li-Chang Lai, Jiaxiang Liu, Xiaomu Shi, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang
2023 — conf
Certified Verification for Algebraic Abstraction.
CAV (3)
Ming-Hsien Tsai, Yu-Fu Fu, Jiaxiang Liu, Xiaomu Shi, Bow-Yaw Wang, Bo-Yin Yang
2023 — conf
CoqCryptoLine: A Verified Model Checker with Certified Results.
CAV (2)
Ming-Hsien Tsai, Yu-Fu Fu, Jiaxiang Liu, Xiaomu Shi, Bow-Yaw Wang, Bo-Yin Yang
2023 — conf
llvm2CryptoLine: Verifying Arithmetic in Cryptographic C Programs.
ESEC/SIGSOFT FSE
Ruiling Chen, Jiaxiang Liu, Xiaomu Shi, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang
2022 J jnl
Automatic Certified Verification of Cryptographic Programs with COQCRYPTOLINE.
IACR Cryptol. ePrint Arch.
Ming-Hsien Tsai, Yu-Fu Fu, Xiaomu Shi, Jiaxiang Liu, Bow-Yaw Wang, Bo-Yin Yang
2022 J jnl
Verified NTT Multiplications for NISTPQC KEM Lattice Finalists: Kyber, SABER, and NTRU.
IACR Trans. Cryptogr. Hardw. Embed. Syst.
Vincent Hwang, Jiaxiang Liu, Gregor Seiler, Xiaomu Shi, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang
2021 — conf
CoqQFBV: A Scalable Certified SMT Quantifier-Free Bit-Vector Solver.
CAV (2)
Xiaomu Shi, Yu-Fu Fu, Jiaxiang Liu, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang
2019 A* conf
Signed Cryptographic Program Verification with Typed CryptoLine.
CCS
Yu-Fu Fu, Jiaxiang Liu, Xiaomu Shi, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang
2019 — conf
Synthesize Models for Quantitative Analysis Using Automata Learning.
NETYS
Yu-Fang Chen, Hsiao-chen Chung, Wen-Chi Hung, Ming-Hsien Tsai, Bow-Yaw Wang, Farn Wang
2019 A* conf
Verifying Arithmetic in Cryptographic C Programs.
ASE
Jiaxiang Liu, Xiaomu Shi, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang
2018 A* conf
Advanced automata-based algorithms for program termination checking.
PLDI
Yu-Fang Chen, Matthias Heizmann, Ondrej Lengál, Yong Li, Ming-Hsien Tsai, Andrea Turrini, Lijun Zhang
2018 B conf
Verifying Arithmetic Assembly Programs in Cryptographic Primitives (Invited Talk).
CONCUR
Andy Polyakov, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang
2017 A* conf
Certified Verification of Algebraic Properties on Low-Level Mathematical Constructs in Cryptographic Programs.
CCS
Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang
2016 — conf
A Targeting Self-breakable Agent for Increased Efficacy of Chemotherapeutic Drugs against Caco2 Cells.
BIODEVICES
Ming-Hsien Tsai, Ming-Jium Shieh, Cheng-Liang Peng
2016 A conf
Complementing Semi-deterministic Büchi Automata.
TACAS
Frantisek Blahoudek, Matthias Heizmann, Sven Schewe, Jan Strejcek, Ming-Hsien Tsai
2016 A* conf
PAC learning-based verification and model synthesis.
ICSE
Yu-Fang Chen, Chiao Hsieh, Ondrej Lengál, Tsung-Ju Lii, Ming-Hsien Tsai, Bow-Yaw Wang, Farn Wang
2015 A conf
CPArec: Verifying Recursive Programs via Source-to-Source Program Transformation - (Competition Contribution).
TACAS
Yu-Fang Chen, Chiao Hsieh, Ming-Hsien Tsai, Bow-Yaw Wang, Farn Wang
2015 J jnl
PAC Learning-Based Verification and Model Synthesis.
CoRR
Yu-Fang Chen, Chiao Hsieh, Ondrej Lengál, Tsung-Ju Lii, Ming-Hsien Tsai, Bow-Yaw Wang, Farn Wang
2014 J jnl
State of Büchi Complementation.
Log. Methods Comput. Sci.
Ming-Hsien Tsai, Seth Fogarty, Moshe Y. Vardi, Yih-Kuen Tsay
2014 A* conf
Verifying Curve25519 Software.
CCS
Yu-Fang Chen, Chang-Hong Hsu, Hsin-hung Lin, Peter Schwabe, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang, Shang-Yi Yang
2014 B conf
Verifying Recursive Programs Using Intraprocedural Analyzers.
SAS
Yu-Fang Chen, Chiao Hsieh, Ming-Hsien Tsai, Bow-Yaw Wang, Farn Wang
2013 J jnl
Büchi Store: an open repository of ω-automata.
Int. J. Softw. Tools Technol. Transf.
Yih-Kuen Tsay, Ming-Hsien Tsai, Jinn-Shu Chang, Yi-Wen Chang, Chi-Shiang Liu
2013 A* conf
GOAL for Games, Omega-Automata, and Logics.
CAV
Ming-Hsien Tsai, Yih-Kuen Tsay, Yu-Shiang Hwang
2011 A conf
Büchi Store: An Open Repository of Büchi Automata.
TACAS
Yih-Kuen Tsay, Ming-Hsien Tsai, Jinn-Shu Chang, Yi-Wen Chang
2010 A* conf
Automated Assume-Guarantee Reasoning through Implicit Learning.
CAV
Yu-Fang Chen, Edmund M. Clarke, Azadeh Farzan, Ming-Hsien Tsai, Yih-Kuen Tsay, Bow-Yaw Wang
2010 A* conf
Automatic numeric abstractions for heap-manipulating programs.
POPL
Stephen Magill, Ming-Hsien Tsai, Peter Lee, Yih-Kuen Tsay
2010 — conf
Comparing Learning Algorithms in Automated Assume-Guarantee Reasoning.
ISoLA (1)
Yu-Fang Chen, Edmund M. Clarke, Azadeh Farzan, Fei He, Ming-Hsien Tsai, Yih-Kuen Tsay, Bow-Yaw Wang, Lei Zhu
2010 C conf
State of Büchi Complementation.
CIAA
Ming-Hsien Tsai, Seth Fogarty, Moshe Y. Vardi, Yih-Kuen Tsay
2009 J jnl
Tool support for learning Büchi automata and linear temporal logic.
Formal Aspects Comput.
Yih-Kuen Tsay, Yu-Fang Chen, Ming-Hsien Tsai, Kang-Nien Wu, Wen-Chin Chan, Chi-Jian Luo, Jinn-Shu Chang
2008 A conf
GOAL Extended: Towards a Research Tool for Omega Automata and Temporal Logic.
TACAS
Yih-Kuen Tsay, Yu-Fang Chen, Ming-Hsien Tsai, Wen-Chin Chan, Chi-Jian Luo
2008 A* conf
THOR: A Tool for Reasoning about Shape and Arithmetic.
CAV
Stephen Magill, Ming-Hsien Tsai, Peter Lee, Yih-Kuen Tsay
2007 A conf
GOAL: A Graphical Tool for Manipulating Büchi Automata and Temporal Formulae.
TACAS
Yih-Kuen Tsay, Yu-Fang Chen, Ming-Hsien Tsai, Kang-Nien Wu, Wen-Chin Chan
2006 — conf
Formalization of CTL* in Calculus of Inductive Constructions.
ASIAN
Ming-Hsien Tsai, Bow-Yaw Wang
2006 — conf
Modular Formalization of Reactive Modules in COQ.
ASIAN
Ming-Hsien Tsai, Bow-Yaw Wang