| Automatic numeric abstractions for heap-manipulating programs S Magill, MH Tsai, P Lee, YK Tsay Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of …, 2010 | 135 | 2010 |
| Verifying curve25519 software YF Chen, CH Hsu, HH Lin, P Schwabe, MH Tsai, BY Wang, BY Yang, ... Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications …, 2014 | 80 | 2014 |
| THOR: A Tool for Reasoning about Shape and Arithmetic: Tool Paper S Magill, MH Tsai, P Lee, YK Tsay International Conference on Computer Aided Verification, 428-432, 2008 | 75 | 2008 |
| Goal: A graphical tool for manipulating büchi automata and temporal formulae YK Tsay, YF Chen, MH Tsai, KN Wu, WC Chan International Conference on Tools and Algorithms for the Construction and …, 2007 | 70 | 2007 |
| Automated assume-guarantee reasoning through implicit learning YF Chen, EM Clarke, A Farzan, MH Tsai, YK Tsay, BY Wang International Conference on Computer Aided Verification, 511-526, 2010 | 69 | 2010 |
| State of B\" uchi Complementation MH Tsai, S Fogarty, MY Vardi, YK Tsay Logical Methods in Computer Science 10, 2014 | 66 | 2014 |
| GOAL for games, omega-automata, and logics MH Tsai, YK Tsay, YS Hwang International Conference on Computer Aided Verification, 883-889, 2013 | 54 | 2013 |
| Complementing semi-deterministic Büchi automata F Blahoudek, M Heizmann, S Schewe, J Strejček, MH Tsai International Conference on Tools and Algorithms for the Construction and …, 2016 | 48 | 2016 |
| Advanced automata-based algorithms for program termination checking YF Chen, M Heizmann, O Lengál, Y Li, MH Tsai, A Turrini, L Zhang Proceedings of the 39th ACM SIGPLAN Conference on Programming Language …, 2018 | 47 | 2018 |
| Certified verification of algebraic properties on low-level mathematical constructs in cryptographic programs MH Tsai, BY Wang, BY Yang Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications …, 2017 | 35 | 2017 |
| Signed cryptographic program verification with typed cryptoline YF Fu, J Liu, X Shi, MH Tsai, BY Wang, BY Yang Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications …, 2019 | 33 | 2019 |
| Verifying arithmetic assembly programs in cryptographic primitives (invited talk) A Polyakov, MH Tsai, BY Wang, BY Yang 29th International Conference on Concurrency Theory (CONCUR 2018), 4: 1-4: 16, 2018 | 32 | 2018 |
| PAC learning-based verification and model synthesis YF Chen, C Hsieh, O Lengál, TJ Lii, MH Tsai, BY Wang, F Wang Proceedings of the 38th International Conference on Software Engineering …, 2016 | 32 | 2016 |
| GOAL extended: Towards a research tool for omega automata and temporal logic YK Tsay, YF Chen, MH Tsai, WC Chan, CJ Luo International Conference on Tools and Algorithms for the Construction and …, 2008 | 29 | 2008 |
| Verified NTT multiplications for NISTPQC KEM lattice finalists: Kyber, SABER, and NTRU V Hwang, J Liu, G Seiler, X Shi, MH Tsai, BY Wang, BY Yang IACR Transactions on Cryptographic Hardware and Embedded Systems, 718-750, 2022 | 23 | 2022 |
| Büchi store: An open repository of Büchi automata YK Tsay, MH Tsai, JS Chang, YW Chang International Conference on Tools and Algorithms for the Construction and …, 2011 | 18 | 2011 |
| Verifying arithmetic in cryptographic C programs J Liu, X Shi, MH Tsai, BY Wang, BY Yang 2019 34th IEEE/ACM International Conference on Automated Software …, 2019 | 17 | 2019 |
| Formalization of CTL* in Calculus of Inductive Constructions MH Tsai, BY Wang Annual Asian Computing Science Conference, 316-330, 2006 | 16 | 2006 |
| CoqQFBV: a scalable certified SMT quantifier-free bit-vector solver X Shi, YF Fu, J Liu, MH Tsai, BY Wang, BY Yang International Conference on Computer Aided Verification, 149-171, 2021 | 14 | 2021 |
| Büchi Store: an open repository of-automata YK Tsay, MH Tsai, JS Chang, YW Chang, CS Liu International Journal on Software Tools for Technology Transfer 15 (2), 109-123, 2013 | 12 | 2013 |