A Unified Approach for Reasoning about Conflict-Free Petri Nets. - Hsu-Chun Yen; Bow-Yaw Wang; Ming-Sheng Yang (Application and Theory of Petri Nets, 1993)

Some Complexity Results for Rings of Petri Nets. - Hsu-Chun Yen; Bow-Yaw Wang; Ming-Sheng Yang (Int. J. Found. Comput. Sci., 1994)

Deciding a Class of Path Formulas for Conflict-Free Petri Nets. - Hsu-Chun Yen; Bow-Yaw Wang; Ming-Sheng Yang (Theory Comput. Syst., 1997)

"Next" Heuristic for On-the-Fly Model Checking. - Rajeev Alur; Bow-Yaw Wang (CONCUR, 1999)

Automated Refinement Checking for Asynchronous Processes. - Rajeev Alur; Radu Grosu; Bow-Yaw Wang (FMCAD, 2000)

Specification and Formal Analysis of a PLAN Algorithm in Maude. - Bow-Yaw Wang; José Meseguer 001; Carl A. Gunter (ICDCS Workshop on Distributed System Validation and Verification, 2000)

Verifying Network Protocol Implementations by Symbolic Refinement Checking. - Rajeev Alur; Bow-Yaw Wang (CAV, 2001)

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 (ICSE, 2001)

Toward Unbounded Model Checking for Region Automata. - Fang Yu 001; Bow-Yaw Wang (ATVA, 2004)

Bounded Model Checking for Region Automata. - Fang Yu 001; Bow-Yaw Wang; Yao-Wen Huang (FORMATS/FTRTFT, 2004)

mu-Calculus Model Checking in Maude. - Bow-Yaw Wang (WRLA, 2004)

BDD-Based Safety-Analysis of Concurrent Software with Pointer Data Structures Using Graph Automorphism Symmetry Reduction. - Farn Wang; Karsten Schmidt 004; Fang Yu 001; Geng-Dian Huang; Bow-Yaw Wang (IEEE Trans. Software Eng., 2004)

Proving forall-µ-Calculus Properties with SAT-Based Model Checking. - Bow-Yaw Wang (FORTE, 2005)

Specification of an Infinite-State Local Model Checker in Rewriting Logic. - Bow-Yaw Wang (SEKE, 2005)

Modular Formalization of Reactive Modules in COQ. - Ming-Hsien Tsai 001; Bow-Yaw Wang (ASIAN, 2006)

Formalization of CTL* in Calculus of Inductive Constructions. - Ming-Hsien Tsai 001; Bow-Yaw Wang (ASIAN, 2006)

On the Satisfiability of Modular Arithmetic Formulae. - Bow-Yaw Wang (ATVA, 2006)

Automatic Verification of a Model Checker by Reflection. - Bow-Yaw Wang (PADL, 2006)

Modeling and analyzing applications with domain-specific languages by reflective rewriting: a case study. - Bow-Yaw Wang (SAC, 2006)

Sat-based Model Checking for Region Automata. - Fang Yu 001; Bow-Yaw Wang (Int. J. Found. Comput. Sci., 2006)

Automatic Derivation of Compositional Rules in Automated Compositional Reasoning. - Bow-Yaw Wang (CONCUR, 2007)

Extending Automated Compositional Verification to the Full Class of Omega-Regular Languages. - Azadeh Farzan; Yu-Fang Chen 001; Edmund M. Clarke; Yih-Kuen Tsay; Bow-Yaw Wang (TACAS, 2008)

Learning Minimal Separating DFA's for Compositional Verification. - Yu-Fang Chen 001; Azadeh Farzan; Edmund M. Clarke; Yih-Kuen Tsay; Bow-Yaw Wang (TACAS, 2009)

Automated Compositional Reasoning of Intuitionistically Closed Regular Properties. - Yih-Kuen Tsay; Bow-Yaw Wang (Int. J. Found. Comput. Sci., 2009)

Automatically Inferring Quantified Loop Invariants by Algorithmic Learning from Simple Templates. - Soonho Kong; Yungbum Jung; Cristina David; Bow-Yaw Wang; Kwangkeun Yi (APLAS, 2010)

Automated Assume-Guarantee Reasoning through Implicit Learning. - Yu-Fang Chen 001; Edmund M. Clarke; Azadeh Farzan; Ming-Hsien Tsai 001; Yih-Kuen Tsay; Bow-Yaw Wang (CAV, 2010)

On Array Theory of Bounded Elements. - Min Zhou 001; Fei He 001; Bow-Yaw Wang; Ming Gu 001 (CAV, 2010)

Comparing Learning Algorithms in Automated Assume-Guarantee Reasoning. - Yu-Fang Chen 001; Edmund M. Clarke; Azadeh Farzan; Fei He 001; Ming-Hsien Tsai 001; Yih-Kuen Tsay; Bow-Yaw Wang; Lei Zhu (ISoLA (1), 2010)

Deriving Invariants by Algorithmic Learning, Decision Procedures, and Predicate Abstraction. - Yungbum Jung; Soonho Kong; Bow-Yaw Wang; Kwangkeun Yi (VMCAI, 2010)

Complete SAT-Based Model Checking for Context-Free Processes. - Geng-Dian Huang; Bow-Yaw Wang (Int. J. Found. Comput. Sci., 2010)

Learning Boolean Functions Incrementally. - Yu-Fang Chen 001; Bow-Yaw Wang (CAV, 2012)

Termination Analysis with Algorithmic Learning. - Wonchan Lee; Bow-Yaw Wang; Kwangkeun Yi (CAV, 2012)

Thread-Modular Model Checking with Iterative Refinement. - Wenrui Meng; Fei He 001; Bow-Yaw Wang; Qiang Liu (NASA Formal Methods, 2012)

Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference - Wonchan Lee; Yungbum Jung; Bow-Yaw Wang; Kwangkeun Yi (Log. Methods Comput. Sci., 2012)

VCS: A Verifier for Component-Based Systems. - Fei He 001; Liangze Yin; Bow-Yaw Wang; Lianyi Zhang; Guanyu Mu; Wenrui Meng (ATVA, 2013)

BULL: A Library for Learning Algorithms of Boolean Functions. - Yu-Fang Chen 001; Bow-Yaw Wang (TACAS, 2013)

A Finite Exact Representation of Register Automata Configurations. - Yu-Fang Chen 001; Bow-Yaw Wang; Di-De Yen (INFINITY, 2013)

A Unified Framework for DPLL(T) + Certificates. - Min Zhou 001; Fei He 001; Bow-Yaw Wang; Ming Gu 001; Jiaguang Sun 001 (J. Appl. Math., 2013)

Learning Summaries of Recursive Functions. - Yu-Fang Chen 001; Bow-Yaw Wang; Kai-Chun Yang (APSEC (1), 2014)

Verifying Curve25519 Software. - Yu-Fang Chen 001; Chang-Hong Hsu; Hsin-Hung Lin; Peter Schwabe; Ming-Hsien Tsai 001; Bow-Yaw Wang; Bo-Yin Yang; Shang-Yi Yang (CCS, 2014)

Symbolic assume-guarantee reasoning through BDD learning. - Fei He 001; Bow-Yaw Wang; Liangze Yin; Lei Zhu (ICSE, 2014)

Verifying Recursive Programs Using Intraprocedural Analyzers. - Yu-Fang Chen 001; Chiao Hsieh; Ming-Hsien Tsai 001; Bow-Yaw Wang; Farn Wang (SAS, 2014)

Array Theory of Bounded Elements and its Applications. - Min Zhou 001; Fei He 001; Bow-Yaw Wang; Ming Gu 001; Jiaguang Sun 001 (J. Autom. Reason., 2014)

Counterexample-Guided Polynomial Loop Invariant Generation by Lagrange Interpolation. - Yu-Fang Chen 001; Chih-Duo Hong; Bow-Yaw Wang; Lijun Zhang 001 (CAV (1), 2015)

Leveraging Weighted Automata in Compositional Reasoning about Concurrent Probabilistic Systems. - Fei He 001; Xiaowei Gao; Bow-Yaw Wang; Lijun Zhang 001 (POPL, 2015)

Commutativity of Reducers. - Yu-Fang Chen 001; Chih-Duo Hong; Nishant Sinha 001; Bow-Yaw Wang (TACAS, 2015)

CPArec: Verifying Recursive Programs via Source-to-Source Program Transformation - (Competition Contribution). - Yu-Fang Chen 001; Chiao Hsieh; Ming-Hsien Tsai 001; Bow-Yaw Wang; Farn Wang (TACAS, 2015)

Automatically inferring loop invariants via algorithmic learning. - Yungbum Jung; Soonho Kong; Cristina David; Bow-Yaw Wang; Kwangkeun Yi (Math. Struct. Comput. Sci., 2015)

Learning-Based Assume-Guarantee Regression Verification. - Fei He 001; Shu Mao; Bow-Yaw Wang (CAV (1), 2016)

PAC learning-based verification and model synthesis. - Yu-Fang Chen 001; Chiao Hsieh; Ondrej Lengál; Tsung-Ju Lii; Ming-Hsien Tsai 001; Bow-Yaw Wang; Farn Wang (ICSE, 2016)

Optimal sanitization synthesis for web application vulnerability repair. - Fang Yu 001; Ching-Yuan Shueh; Chun-Han Lin; Yu-Fang Chen 001; Bow-Yaw Wang; Tevfik Bultan (ISSTA, 2016)

Learning Weighted Assumptions for Compositional Verification of Markov Decision Processes. - Fei He 001; Xiaowei Gao; Miaofei Wang; Bow-Yaw Wang; Lijun Zhang 001 (ACM Trans. Softw. Eng. Methodol., 2016)

Certified Verification of Algebraic Properties on Low-Level Mathematical Constructs in Cryptographic Programs. - Ming-Hsien Tsai 001; Bow-Yaw Wang; Bo-Yin Yang (CCS, 2017)

PSpec: a formal specification language for fine-grained control on distributed data analytics. - Chen Luo 002; Fei He 001; Dong Yan; Dan Zhang; Xin Zhou; Bow-Yaw Wang (ICSE (Companion Volume), 2017)

Releasing VDM proof obligations with SMT solvers. - Hsin-Hung Lin; Bow-Yaw Wang (MEMOCODE, 2017)

An Executable Sequential Specification for Spark Aggregation. - Yu-Fang Chen 001; Chih-Duo Hong; Ondrej Lengál; Shin-Cheng Mu; Nishant Sinha 001; Bow-Yaw Wang (NETYS, 2017)

Model Checking Differentially Private Properties. - Depeng Liu; Bow-Yaw Wang; Lijun Zhang 001 (APLAS, 2018)

Verifying Arithmetic Assembly Programs in Cryptographic Primitives (Invited Talk). - Andy Polyakov; Ming-Hsien Tsai 001; Bow-Yaw Wang; Bo-Yin Yang (CONCUR, 2018)

A Spin-based model checking for the simple concurrent program on a preemptive RTOS. - Chen-Kai Lin; Ching-Chun Huang; Bow-Yaw Wang (CoRR, 2018)

Signed Cryptographic Program Verification with Typed CryptoLine. - Yu-Fu Fu; Jiaxiang Liu 001; Xiaomu Shi; Ming-Hsien Tsai 001; Bow-Yaw Wang; Bo-Yin Yang (CCS, 2019)

Parameterized Hardware Verification Through a Term-Level Generalized Symbolic Trajectory Evaluation. - Yongjian Li; Bow-Yaw Wang (ICFEM, 2019)

Verifying Arithmetic in Cryptographic C Programs. - Jiaxiang Liu 001; Xiaomu Shi; Ming-Hsien Tsai 001; Bow-Yaw Wang; Bo-Yin Yang (ASE, 2019)

Synthesize Models for Quantitative Analysis Using Automata Learning. - Yu-Fang Chen 001; Hsiao-chen Chung; Wen-Chi Hung; Ming-Hsien Tsai 001; Bow-Yaw Wang; Farn Wang (NETYS, 2019)

Interval counterexamples for loop invariant learning. - Rongchen Xu; Fei He 001; Bow-Yaw Wang (ESEC/SIGSOFT FSE, 2020)

Incremental predicate analysis for regression verification. - Qianshan Yu; Fei He 001; Bow-Yaw Wang (Proc. ACM Program. Lang., 2020)

CoqQFBV: A Scalable Certified SMT Quantifier-Free Bit-Vector Solver. - Xiaomu Shi; Yu-Fu Fu; Jiaxiang Liu 001; Ming-Hsien Tsai 001; Bow-Yaw Wang; Bo-Yin Yang (CAV (2), 2021)

Verifying Pufferfish Privacy in Hidden Markov Models. - Depeng Liu; Bow-Yaw Wang; Lijun Zhang 001 (VMCAI, 2022)

Defensive Design of Saturating Counters Based on Differential Privacy. - Depeng Liu; Lutan Zhao; Pengfei Yang 002; Bow-Yaw Wang; Rui Hou 001; Lijun Zhang 001; Naijun Zhan (CoRR, 2022)

Automatic Certified Verification of Cryptographic Programs with COQCRYPTOLINE. - Ming-Hsien Tsai 001; Yu-Fu Fu; Xiaomu Shi; Jiaxiang Liu 001; Bow-Yaw Wang; Bo-Yin Yang (IACR Cryptol. ePrint Arch., 2022)

Verified NTT Multiplications for NISTPQC KEM Lattice Finalists: Kyber, SABER, and NTRU. - Vincent Hwang; Jiaxiang Liu 001; Gregor Seiler; Xiaomu Shi; Ming-Hsien Tsai 001; Bow-Yaw Wang; Bo-Yin Yang (IACR Trans. Cryptogr. Hardw. Embed. Syst., 2022)

Certified Verification for Algebraic Abstraction. - Ming-Hsien Tsai 001; Yu-Fu Fu; Jiaxiang Liu 001; Xiaomu Shi; Bow-Yaw Wang; Bo-Yin Yang (CAV (3), 2023)

CoqCryptoLine: A Verified Model Checker with Certified Results. - Ming-Hsien Tsai 001; Yu-Fu Fu; Jiaxiang Liu 001; Xiaomu Shi; Bow-Yaw Wang; Bo-Yin Yang (CAV (2), 2023)

llvm2CryptoLine: Verifying Arithmetic in Cryptographic C Programs. - Ruiling Chen; Jiaxiang Liu 001; Xiaomu Shi; Ming-Hsien Tsai 001; Bow-Yaw Wang; Bo-Yin Yang (ESEC/SIGSOFT FSE, 2023)

Automatic Verification of Cryptographic Block Function Implementations with Logical Equivalence Checking. - Li-Chang Lai; Jiaxiang Liu 001; Xiaomu Shi; Ming-Hsien Tsai 001; Bow-Yaw Wang; Bo-Yin Yang (IACR Cryptol. ePrint Arch., 2023)

Model checking differentially private properties. - Depeng Liu; Bow-Yaw Wang; Chen Fu; Lijun Zhang 001 (Theor. Comput. Sci., 2023)

Formal Analysis of FreeRTOS Scheduler on ARM Cortex-M4 Cores. - Chen-Kai Lin; Bow-Yaw Wang (ICFEM, 2024)

Ensuring Fairness with Transparent Auditing of Quantitative Bias in AI Systems. - Chih-Cheng Rex Yuan; Bow-Yaw Wang (CoRR, 2024)

Algebraic Linear Analysis for Number Theoretic Transform in Lattice-Based Cryptography. - Chun-Ming Chiu; Jiaxiang Liu 001; Ming-Hsien Tsai 001; Xiaomu Shi; Bow-Yaw Wang; Bo-Yin Yang (IACR Trans. Cryptogr. Hardw. Embed. Syst., 2025)

Quantitative Auditing of AI Fairness with Differentially Private Synthetic Data. - Chih-Cheng Rex Yuan; Bow-Yaw Wang (CoRR, 2025)

SAT-Solving the Poset Cover Problem. - Chih-Cheng Rex Yuan; Bow-Yaw Wang (CoRR, 2025)