Travelled to:1 × Canada
1 × Hungary
1 × Portugal
1 × Russia
1 × Spain
1 × USA
2 × Germany
2 × United Kingdom
Collaborated with:Y.Tsay Y.Chen B.Wang S.Magill P.Lee C.Hsieh F.Wang W.Chan Y.Hwang J.Chang Y.Chang S.Fogarty M.Y.Vardi C.Luo K.Wu J.Liu X.Shi B.Yang E.M.Clarke A.Farzan M.Heizmann O.Lengál Yong Li 0031 A.Turrini L.Z.0001
Talks about:program (6) automata (5) büchi (4) verifi (3) tool (3) goal (3) arithmet (2) manipul (2) tempor (2) recurs (2)
Person: Ming-Hsien Tsai
DBLP: Tsai:Ming=Hsien
Contributed to:
2015
2014
201320112010
2010
2010200820082007
2019
2018Wrote 12 papers:
- TACAS-2015-ChenHTWW #contest #named #program transformation #recursion #source code #text-to-text #verification
- CPArec: Verifying Recursive Programs via Source-to-Source Program Transformation — (Competition Contribution) (YFC, CH, MHT, BYW, FW), pp. 426–428.
- SAS-2014-ChenHTWW #recursion #source code #using #verification
- Verifying Recursive Programs Using Intraprocedural Analyzers (YFC, CH, MHT, BYW, FW), pp. 118–133.
- CAV-2013-TsaiTH #automaton #game studies #logic
- GOAL for Games, ω-Automata, and Logics (MHT, YKT, YSH), pp. 883–889.
- TACAS-2011-TsayTCC #automaton #repository
- Büchi Store: An Open Repository of Büchi Automata (YKT, MHT, JSC, YWC), pp. 262–266.
- CAV-2010-ChenCFTTW #automation #learning #reasoning
- Automated Assume-Guarantee Reasoning through Implicit Learning (YFC, EMC, AF, MHT, YKT, BYW), pp. 511–526.
- CIAA-2010-TsaiFVT #automaton
- State of Büchi Complementation (MHT, SF, MYV, YKT), pp. 261–271.
- POPL-2010-MagillTLT #abstraction #automation #source code
- Automatic numeric abstractions for heap-manipulating programs (SM, MHT, PL, YKT), pp. 211–222.
- CAV-2008-MagillTLT #named #reasoning
- THOR: A Tool for Reasoning about Shape and Arithmetic (SM, MHT, PL, YKT), pp. 428–432.
- TACAS-2008-TsayCTCL #automaton #logic #research #towards
- GOAL Extended: Towards a Research Tool for ω Automata and Temporal Logic (YKT, YFC, MHT, WCC, CJL), pp. 346–350.
- TACAS-2007-TsayCTWC #automaton #named #visual notation
- GOAL: A Graphical Tool for Manipulating Büchi Automata and Temporal Formulae (YKT, YFC, MHT, KNW, WCC), pp. 466–471.
- ASE-2019-LiuSTWY #c #encryption #source code #verification
- Verifying Arithmetic in Cryptographic C Programs (JL, XS, MHT, BYW, BYY), pp. 552–564.
- PLDI-2018-ChenHLLTTZ #algorithm #termination
- Advanced automata-based algorithms for program termination checking (YFC, MH, OL, YL0, MHT, AT, LZ0), pp. 135–150.