Ming-Hsien Tsai
Publication record assembled from the DBLP archive of ranked conferences.
Papers indexed
24
Venues
11
Active years
2007–2025
Best venue rank
A*
Where they publish
Papers
24 indexed papers, newest first.
| Year | Venue | Title | Authors |
|---|---|---|---|
| 2025 | CCS | Jazzline: Composable CryptoLine Functional Correctness Proofs for Jasmin Programs. | Jos Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Lionel Blatter, Gustavo Xavier Delerue Marinho Alves, Joo Diogo Duarte, Benjamin Grgoire, Tiago Oliveira, Miguel Quaresma, Pierre-Yves Strub, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang |
| 2024 | ESORICS | 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 |
| 2023 | CAV | Certified Verification for Algebraic Abstraction. | Ming-Hsien Tsai, Yu-Fu Fu, Jiaxiang Liu, Xiaomu Shi, Bow-Yaw Wang, Bo-Yin Yang |
| 2023 | CAV | CoqCryptoLine: A Verified Model Checker with Certified Results. | Ming-Hsien Tsai, Yu-Fu Fu, Jiaxiang Liu, Xiaomu Shi, Bow-Yaw Wang, Bo-Yin Yang |
| 2021 | CAV | 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 |
| 2019 | CCS | Signed Cryptographic Program Verification with Typed CryptoLine. | Yu-Fu Fu, Jiaxiang Liu, Xiaomu Shi, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang |
| 2018 | CONCUR | Verifying Arithmetic Assembly Programs in Cryptographic Primitives (Invited Talk). | Andy Polyakov, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang |
| 2018 | PLDI | Advanced automata-based algorithms for program termination checking. | Yu-Fang Chen, Matthias Heizmann, Ondrej Lengl, Yong Li, Ming-Hsien Tsai, Andrea Turrini, Lijun Zhang |
| 2017 | CCS | Certified Verification of Algebraic Properties on Low-Level Mathematical Constructs in Cryptographic Programs. | Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang |
| 2016 | ICSE | PAC learning-based verification and model synthesis. | Yu-Fang Chen, Chiao Hsieh, Ondrej Lengl, Tsung-Ju Lii, Ming-Hsien Tsai, Bow-Yaw Wang, Farn Wang |
| 2016 | TACAS | Complementing Semi-deterministic Bchi Automata. | Frantisek Blahoudek, Matthias Heizmann, Sven Schewe, Jan Strejcek, Ming-Hsien Tsai |
| 2015 | TACAS | 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 |
| 2014 | CCS | 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 |
| 2014 | ISCAS | ESD protection design for wideband RF applications in 65-nm CMOS process. | Li-Wei Chu, Chun-Yu Lin, Ming-Dou Ker, Ming-Hsiang Song, Jeng-Chou Tseng, Chewnpu Jou, Ming-Hsien Tsai |
| 2014 | SAS | Verifying Recursive Programs Using Intraprocedural Analyzers. | Yu-Fang Chen, Chiao Hsieh, Ming-Hsien Tsai, Bow-Yaw Wang, Farn Wang |
| 2013 | CAV | GOAL for Games, Omega-Automata, and Logics. | Ming-Hsien Tsai, Yih-Kuen Tsay, Yu-Shiang Hwang |
| 2012 | ISCAS | Compact and low-loss ESD protection design for V-band RF applications in a 65-nm CMOS technology. | 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 |
| 2011 | TACAS | Bchi Store: An Open Repository of Bchi Automata. | Yih-Kuen Tsay, Ming-Hsien Tsai, Jinn-Shu Chang, Yi-Wen Chang |
| 2010 | CAV | Automated Assume-Guarantee Reasoning through Implicit Learning. | Yu-Fang Chen, Edmund M. Clarke, Azadeh Farzan, Ming-Hsien Tsai, Yih-Kuen Tsay, Bow-Yaw Wang |
| 2010 | ISoLA | 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 |
| 2010 | POPL | Automatic numeric abstractions for heap-manipulating programs. | Stephen Magill, Ming-Hsien Tsai, Peter Lee, Yih-Kuen Tsay |
| 2008 | CAV | THOR: A Tool for Reasoning about Shape and Arithmetic. | Stephen Magill, Ming-Hsien Tsai, Peter Lee, Yih-Kuen Tsay |
| 2008 | TACAS | 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 |
| 2007 | TACAS | GOAL: A Graphical Tool for Manipulating Bchi Automata and Temporal Formulae. | Yih-Kuen Tsay, Yu-Fang Chen, Ming-Hsien Tsai, Kang-Nien Wu, Wen-Chin Chan |