I am currently a PhD student in National Taiwan University. My research interests include temporal logic, omega automata, heap analysis, software verification and software security.
Contact: Xmhtsai208@gmail.comX (remove the first and the last X)
Publications
- Yih-Kuen Tsay, Ming-Hsien Tsai, Jinn-Shu Chang, and Yi-Wen Chang. Büchi Store: An Open Repository of Büchi Automata. To appear in TACAS 2011.
- Ming-Hsien Tsai, Seth Fogarty, Moshe Y. Vardi, and Yih-Kuen Tsay: State of Büchi Complementation. CIAA 2010: 261-271.
- 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.
- Yu-Fang Chen, Edmund Clarke, Azadeh Farzan, Ming-Hsien Tsai, Yih-Kuen Tsay and Bow-Yaw Wang: Automated Assume-Guarantee Reasoning through Implicit Learning. CAV 2010: 511-526.
- Stephen Magill, Ming-Hsien Tsai, Peter Lee, Yih-Kuen Tsay: Automatic Numeric Abstractions for Heap-Manipulating Programs. POPL 2010: 211-222.
- 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 Asp. Comput. 21(3): 259-275 (2009).
- Stephen Magill, Ming-Hsien Tsai, Peter Lee, Yih-Kuen Tsay: THOR: A Tool for Reasoning about Shape and Arithmetic. CAV 2008: 428-432.
- 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.
- 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.
- Ming-Hsien Tsai, Bow-Yaw Wang: Modular Formalization of Reactive Modules in COQ. ASIAN 2006: 105-119.
- Ming-Hsien Tsai, Bow-Yaw Wang: Formalization of CTL* in Calculus of Inductive Constructions. ASIAN 2006: 316-330.
Projects / Tools
Research projects and tools:
- OMocha: a μ-calculus/CTL/LTL model checker for reactive modules
- iCAST (2006/09 - 2009/??)
- GOAL: a tool for games, ω-automata, and temporal logics
- THOR: a tool for heap oriented reasoning
- Büchi Store: an online repository of Büchi automata
Personal interests:
- XHTML Validator for Wordpress (WPXV) (obsolote)
- MediaWiki Markup for WordPress (obsolote)
- Java Chinese Book Reader (JCBR): a PDB reader for Chinese books made by mPBD.
- fmport: a Gentoo overlay for formal verification
- doctor: an atuomatic doctor scheduler
Interests
Music
- Japanese：夏川りみ, Melody, Mink, Misia, 一青窈, 大塚愛 恋愛写真, 中孝介, 平原綾香, 竹内まりや, Chage & Aska
- Korean：궁 (宮) OST, 그대 웃어요 (你笑了) OST, 마이걸 (My Girl) OST, 미남이시네요 (是美男阿) OST, 불량커플 (不良情侶) OST, 일지매 (一枝梅) OST, 쾌걸춘향 (豪傑春香) OST, 환상의 커플 (幻想情侶) OST, 시티홀 (City Hall 市政廳) OST
- Taiwanese：江蕙, 黃妃 相思聲聲
- English：Sarah Brightman
- Other：Kevin Kern, Chuck Brown, 賈鵬芳, 千住明, 呂秀齡 (Shirley Lu)
Television
- Japanese：白い巨塔, 古畑任三郎, トリック Trick, パパとムスメの7日間, Hero, マイ ボス マイ ヒーロー, 結婚できない男, のだめカンタービレ, 砂の器, 美女か野獣, 空から降る一億の星, 眠れる森, Beautiful Life, Love Generation, ムコ殿, ハケンの品格, アンフェア Unfair, One Piece, 勇者王ガオガイガー, 機動戦艦ナデシコ, 今日から俺は, 天使な小生意気
- Korean：환상의 커플 (Fantasy Couple, 幻想情侶), 일지매 (一枝梅), 미남이시네요 (是美男啊), 마이걸 (My Girl)
- English：Friends, Prison Break Season 1
發表文章
