| 2026 | EuroCrypt | Accelerating and verifying constant-time modular inversion. | Daniel J. Bernstein, Han-Ting Chen, John R. Harrison, Cesare Huang, Gregory Maxwell, Bow-Yaw Wang, Pieter Wuille, Bo-Yin Yang |
| 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 |
| 2024 | ICFEM | Formal Analysis of FreeRTOS Scheduler on ARM Cortex-M4 Cores. | Chen-Kai Lin, Bow-Yaw Wang |
| 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 |
| 2022 | VMCAI | Verifying Pufferfish Privacy in Hidden Markov Models. | Depeng Liu, Bow-Yaw Wang, Lijun Zhang |
| 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 |
| 2019 | ICFEM | Parameterized Hardware Verification Through a Term-Level Generalized Symbolic Trajectory Evaluation. | Yongjian Li, Bow-Yaw Wang |
| 2018 | APLAS | Model Checking Differentially Private Properties. | Depeng Liu, Bow-Yaw Wang, Lijun Zhang |
| 2018 | CONCUR | Verifying Arithmetic Assembly Programs in Cryptographic Primitives (Invited Talk). | Andy Polyakov, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang |
| 2017 | CCS | Certified Verification of Algebraic Properties on Low-Level Mathematical Constructs in Cryptographic Programs. | Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang |
| 2017 | ICSE | PSpec: a formal specification language for fine-grained control on distributed data analytics. | Chen Luo, Fei He, Dong Yan, Dan Zhang, Xin Zhou, Bow-Yaw Wang |
| 2017 | MEMOCODE | Releasing VDM proof obligations with SMT solvers. | Hsin-Hung Lin, Bow-Yaw Wang |
| 2016 | CAV | Learning-Based Assume-Guarantee Regression Verification. | Fei He, Shu Mao, Bow-Yaw Wang |
| 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 | ISSTA | Optimal sanitization synthesis for web application vulnerability repair. | Fang Yu, Ching-Yuan Shueh, Chun-Han Lin, Yu-Fang Chen, Bow-Yaw Wang, Tevfik Bultan |
| 2015 | CAV | Counterexample-Guided Polynomial Loop Invariant Generation by Lagrange Interpolation. | Yu-Fang Chen, Chih-Duo Hong, Bow-Yaw Wang, Lijun Zhang |
| 2015 | POPL | Leveraging Weighted Automata in Compositional Reasoning about Concurrent Probabilistic Systems. | Fei He, Xiaowei Gao, Bow-Yaw Wang, Lijun Zhang |
| 2015 | TACAS | Commutativity of Reducers. | Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, Bow-Yaw Wang |
| 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 | APSEC | Learning Summaries of Recursive Functions. | Yu-Fang Chen, Bow-Yaw Wang, Kai-Chun Yang |
| 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 | ICSE | Symbolic assume-guarantee reasoning through BDD learning. | Fei He, Bow-Yaw Wang, Liangze Yin, Lei Zhu |
| 2014 | SAS | Verifying Recursive Programs Using Intraprocedural Analyzers. | Yu-Fang Chen, Chiao Hsieh, Ming-Hsien Tsai, Bow-Yaw Wang, Farn Wang |
| 2013 | ATVA | VCS: A Verifier for Component-Based Systems. | Fei He, Liangze Yin, Bow-Yaw Wang, Lianyi Zhang, Guanyu Mu, Wenrui Meng |
| 2013 | TACAS | BULL: A Library for Learning Algorithms of Boolean Functions. | Yu-Fang Chen, Bow-Yaw Wang |
| 2012 | CAV | Learning Boolean Functions Incrementally. | Yu-Fang Chen, Bow-Yaw Wang |
| 2012 | CAV | Termination Analysis with Algorithmic Learning. | Wonchan Lee, Bow-Yaw Wang, Kwangkeun Yi |
| 2011 | TACAS | Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference. | Yungbum Jung, Wonchan Lee, Bow-Yaw Wang, Kwangkeun Yi |
| 2010 | APLAS | Automatically Inferring Quantified Loop Invariants by Algorithmic Learning from Simple Templates. | Soonho Kong, Yungbum Jung, Cristina David, Bow-Yaw Wang, Kwangkeun Yi |
| 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 | CAV | On Array Theory of Bounded Elements. | Min Zhou, Fei He, Bow-Yaw Wang, Ming Gu |
| 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 | VMCAI | Deriving Invariants by Algorithmic Learning, Decision Procedures, and Predicate Abstraction. | Yungbum Jung, Soonho Kong, Bow-Yaw Wang, Kwangkeun Yi |
| 2009 | TACAS | Learning Minimal Separating DFA's for Compositional Verification. | Yu-Fang Chen, Azadeh Farzan, Edmund M. Clarke, Yih-Kuen Tsay, Bow-Yaw Wang |
| 2008 | TACAS | Extending Automated Compositional Verification to the Full Class of Omega-Regular Languages. | Azadeh Farzan, Yu-Fang Chen, Edmund M. Clarke, Yih-Kuen Tsay, Bow-Yaw Wang |
| 2007 | ATVA | Complete SAT-Based Model Checking for Context-Free Processes. | Geng-Dian Huang, Bow-Yaw Wang |
| 2007 | CONCUR | Automatic Derivation of Compositional Rules in Automated Compositional Reasoning. | Bow-Yaw Wang |
| 2006 | ATVA | On the Satisfiability of Modular Arithmetic Formulae. | Bow-Yaw Wang |
| 2006 | PADL | Automatic Verification of a Model Checker by Reflection. | Bow-Yaw Wang |
| 2006 | SAC | Modeling and analyzing applications with domain-specific languages by reflective rewriting: a case study. | Bow-Yaw Wang |
| 2005 | FORTE | Proving forall--Calculus Properties with SAT-Based Model Checking. | Bow-Yaw Wang |
| 2005 | SEKE | Specification of an Infinite-State Local Model Checker in Rewriting Logic. | Bow-Yaw Wang |
| 2004 | ATVA | Toward Unbounded Model Checking for Region Automata. | Fang Yu, Bow-Yaw Wang |
| 2001 | CAV | Verifying Network Protocol Implementations by Symbolic Refinement Checking. | Rajeev Alur, Bow-Yaw Wang |
| 2001 | ICSE | JMOCHA: A Model Checking Tool that Exploits Design Structure. | Rajeev Alur, Luca de Alfaro, Radu Grosu, Thomas A. Henzinger, M. Kang, Christoph M. Kirsch, Rupak Majumdar, Freddy Y. C. Mang, Bow-Yaw Wang |
| 2000 | FMCAD | Automated Refinement Checking for Asynchronous Processes. | Rajeev Alur, Radu Grosu, Bow-Yaw Wang |
| 1999 | CONCUR | "Next" Heuristic for On-the-Fly Model Checking. | Rajeev Alur, Bow-Yaw Wang |