Postdoc Researcher

Institute of Information Science

Academia Sinica

Email: Xmhtsai208@gmail.comX (remove the first and the last X)

Publications

The full publication list is available on DBLP.

• Andy Polyakov, Ming-Hsien Tsai, Bow-Yaw Wang, and Bo-Yin Yang. Verifying Arithmetic Assembly Programs in Cryptographic Primitives (Invited Talk). CONCUR 2018: 4:1-4:16.
• Yu-Fang Chen, Matthias Heizmann, Ondrej Lengál, Yong Li, Ming-Hsien Tsai, Andrea Turrini, and Lijun Zhang. Advanced automata-based algorithms for program termination checking. PLDI 2018: 135-150.
• Ming-Hsien Tsai, Bow-Yaw Wang, and Bo-Yin Yang. Certified Verification of Algebraic Properties on Low-Level Mathematical Constructs in Cryptographic Programs. ACM Conference on Computer and Communications Security 2017: 1973-1987.
• Yu-Fang Chen, Chiao Hsieh, Ondrej Lengál, Tsung-Ju Lii, Ming-Hsien Tsai, Bow-Yaw Wang, and Farn Wang. PAC learning-based verification and model synthesis. ICSE 2016: 714-724.
• Frantisek Blahoudek, Matthias Heizmann, Sven Schewe, Jan Strejcek, and Ming-Hsien Tsai. Complementing Semi-deterministic Büchi Automata. TACAS 2016: 770-787.

Tools

• GOAL: a tool for games, ω-automata, and temporal logics
• Büchi Store: an online repository of Büchi automata
• THOR: a tool for heap oriented reasoning
• CPARec: tool for verifying recursive C programs via source-to-source program transformation
• certified-constructs, certified_qhasm_vcg: a certified verification tool for low-level implementations of mathematical constructs in cryptographic programs
• homebrew-formal: a tap containing some verification related tools for Homebrew