default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDMing-Hsien Tsai 0001
Person information
- affiliation: National Applied Research Labs, Taipei, Taiwan
- affiliation: Academia Sinica, Taipei City, Taiwan
- affiliation (former): National Taiwan University, Taipei, Taiwan
Other persons with the same name
- Ming-Hsien Tsai 0002 — Taiwan Semiconductor Manufacturing Company Limited (TSMC), Hsinchu, Taiwan
- Ming-Hsien Tsai 0003 — Da-Yeh University, Taiwan
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2024
[c28]Li-Chang Lai, Jiaxiang Liu, Xiaomu Shi, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang:
Automatic Verification of Cryptographic Block Function Implementations with Logical Equivalence Checking. ESORICS (4) 2024: 377-395- 2023
- [c27]Ming-Hsien Tsai, Yu-Fu Fu, Jiaxiang Liu, Xiaomu Shi, Bow-Yaw Wang, Bo-Yin Yang:
CoqCryptoLine: A Verified Model Checker with Certified Results. CAV (2) 2023: 227-240 - [c26]Ming-Hsien Tsai, Yu-Fu Fu, Jiaxiang Liu, Xiaomu Shi, Bow-Yaw Wang, Bo-Yin Yang:
Certified Verification for Algebraic Abstraction. CAV (3) 2023: 329-349 - [c25]Ruiling Chen
, Jiaxiang Liu, Xiaomu Shi, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang:
llvm2CryptoLine: Verifying Arithmetic in Cryptographic C Programs. ESEC/SIGSOFT FSE 2023: 2167-2171 - [i3]Li-Chang Lai, Jiaxiang Liu, Xiaomu Shi, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang:
Automatic Verification of Cryptographic Block Function Implementations with Logical Equivalence Checking. IACR Cryptol. ePrint Arch. 2023: 1861 (2023) - 2022
- [j4]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): 718-750 (2022) - [i2]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: 1116 (2022) - 2021
- [c24]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: 149-171
2010 – 2019
- 2019
- [c23]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: 1591-1606 - [c22]Jiaxiang Liu, Xiaomu Shi, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang:
Verifying Arithmetic in Cryptographic C Programs. ASE 2019: 552-564 - [c21]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: 75-92 - 2018
- [c20]Andy Polyakov, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang:
Verifying Arithmetic Assembly Programs in Cryptographic Primitives (Invited Talk). CONCUR 2018: 4:1-4:16 - [c19]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: 135-150 - 2017
- [c18]Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang:
Certified Verification of Algebraic Properties on Low-Level Mathematical Constructs in Cryptographic Programs. CCS 2017: 1973-1987 - 2016
- [c17]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: 216-221 - [c16]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: 714-724 - [c15]Frantisek Blahoudek, Matthias Heizmann, Sven Schewe, Jan Strejcek, Ming-Hsien Tsai:
Complementing Semi-deterministic Büchi Automata. TACAS 2016: 770-787 - 2015
- [c14]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: 426-428 - [i1]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 abs/1511.00754 (2015) - 2014
- [j3]Ming-Hsien Tsai, Seth Fogarty, Moshe Y. Vardi, Yih-Kuen Tsay:
State of Büchi Complementation. Log. Methods Comput. Sci. 10(4) (2014) - [c13]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: 299-309 - [c12]Yu-Fang Chen, Chiao Hsieh, Ming-Hsien Tsai, Bow-Yaw Wang, Farn Wang:
Verifying Recursive Programs Using Intraprocedural Analyzers. SAS 2014: 118-133 - 2013
- [j2]Yih-Kuen Tsay, Ming-Hsien Tsai, Jinn-Shu Chang, Yi-Wen Chang, Chi-Shiang Liu:
Büchi Store: an open repository of ω-automata. Int. J. Softw. Tools Technol. Transf. 15(2): 109-123 (2013) - [c11]Ming-Hsien Tsai, Yih-Kuen Tsay, Yu-Shiang Hwang:
GOAL for Games, Omega-Automata, and Logics. CAV 2013: 883-889 - 2011
- [c10]Yih-Kuen Tsay, Ming-Hsien Tsai, Jinn-Shu Chang, Yi-Wen Chang:
Büchi Store: An Open Repository of Büchi Automata. TACAS 2011: 262-266 - 2010
- [c9]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: 511-526 - [c8]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: 643-657 - [c7]Stephen Magill, Ming-Hsien Tsai, Peter Lee, Yih-Kuen Tsay:
Automatic numeric abstractions for heap-manipulating programs. POPL 2010: 211-222 - [c6]Ming-Hsien Tsai, Seth Fogarty, Moshe Y. Vardi, Yih-Kuen Tsay:
State of Büchi Complementation. CIAA 2010: 261-271
2000 – 2009
- 2009
- [j1]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): 259-275 (2009) - 2008
- [c5]Stephen Magill, Ming-Hsien Tsai, Peter Lee, Yih-Kuen Tsay:
THOR: A Tool for Reasoning about Shape and Arithmetic. CAV 2008: 428-432 - [c4]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: 346-350 - 2007
- [c3]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: 466-471 - 2006
- [c2]Ming-Hsien Tsai, Bow-Yaw Wang:
Modular Formalization of Reactive Modules in COQ. ASIAN 2006: 105-119 - [c1]Ming-Hsien Tsai, Bow-Yaw Wang:
Formalization of CTL* in Calculus of Inductive Constructions. ASIAN 2006: 316-330
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-10-07 22:13 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
