Bow-Yaw Wang

Publication Activity (10 Years)

Years Active: 1993-2023
Publications (10 Years): 37

Top Topics

Recursive Programs

Formal Specification

Top Venues

ESEC/SIGSOFT FSE

Publications

Ming-Hsien Tsai, Yu-Fu Fu, Jiaxiang Liu, Xiaomu Shi, Bow-Yaw Wang, Bo-Yin Yang
Certified Verification for Algebraic Abstraction. CAV (3) (2023)
Ruiling Chen, Jiaxiang Liu, Xiaomu Shi, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang
llvm2CryptoLine: Verifying Arithmetic in Cryptographic C Programs. ESEC/SIGSOFT FSE (2023)
Depeng Liu, Bow-Yaw Wang, Chen Fu, Lijun Zhang
Model checking differentially private properties. Theor. Comput. Sci. 943 (2023)
Li-Chang Lai, Jiaxiang Liu, Xiaomu Shi, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang
Automatic Verification of Cryptographic Block Function Implementations with Logical Equivalence Checking. IACR Cryptol. ePrint Arch. 2023 (2023)
Ming-Hsien Tsai, Yu-Fu Fu, Jiaxiang Liu, Xiaomu Shi, Bow-Yaw Wang, Bo-Yin Yang
CoqCryptoLine: A Verified Model Checker with Certified Results. CAV (2) (2023)
Depeng Liu, Bow-Yaw Wang, Lijun Zhang
Verifying Pufferfish Privacy in Hidden Markov Models. VMCAI (2022)
Vincent Hwang, Jiaxiang Liu, Gregor Seiler, Xiaomu Shi, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang
Verified NTT Multiplications for NISTPQC KEM Lattice Finalists: Kyber, SABER, and NTRU. IACR Trans. Cryptogr. Hardw. Embed. Syst. 2022 (4) (2022)
Depeng Liu, Lutan Zhao, Pengfei Yang, Bow-Yaw Wang, Rui Hou, Lijun Zhang, Naijun Zhan
Defensive Design of Saturating Counters Based on Differential Privacy. CoRR (2022)
Chen-Kai Lin, Bow-Yaw Wang
Formal Analysis of FreeRTOS Scheduler on ARM Cortex-M4 Cores. CoRR (2022)
Ming-Hsien Tsai, Yu-Fu Fu, Xiaomu Shi, Jiaxiang Liu, Bow-Yaw Wang, Bo-Yin Yang
Automatic Certified Verification of Cryptographic Programs with COQCRYPTOLINE. IACR Cryptol. ePrint Arch. 2022 (2022)
Xiaomu Shi, Yu-Fu Fu, Jiaxiang Liu, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang
CoqQFBV: A Scalable Certified SMT Quantifier-Free Bit-Vector Solver. CAV (2) (2021)
Rongchen Xu, Fei He, Bow-Yaw Wang
Interval counterexamples for loop invariant learning. ESEC/SIGSOFT FSE (2020)
Qianshan Yu, Fei He, Bow-Yaw Wang
Incremental predicate analysis for regression verification. Proc. ACM Program. Lang. 4 (OOPSLA) (2020)
Depeng Liu, Bow-Yaw Wang, Lijun Zhang
Verifying Pufferfish Privacy in Hidden Markov Models. CoRR (2020)
Yu-Fu Fu, Jiaxiang Liu, Xiaomu Shi, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang
Signed Cryptographic Program Verification with Typed CryptoLine. CCS (2019)
Yu-Fang Chen, Hsiao-chen Chung, Wen-Chi Hung, Ming-Hsien Tsai, Bow-Yaw Wang, Farn Wang
Synthesize Models for Quantitative Analysis Using Automata Learning. NETYS (2019)
Jiaxiang Liu, Xiaomu Shi, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang
Verifying Arithmetic in Cryptographic C Programs. ASE (2019)
Yongjian Li, Bow-Yaw Wang
Parameterized Hardware Verification Through a Term-Level Generalized Symbolic Trajectory Evaluation. ICFEM (2019)
Depeng Liu, Bow-Yaw Wang, Lijun Zhang
Model Checking Differentially Private Properties. APLAS (2018)
Chen-Kai Lin, Ching-Chun Huang, Bow-Yaw Wang
A Spin-based model checking for the simple concurrent program on a preemptive RTOS. CoRR (2018)
Andy Polyakov, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang
Verifying Arithmetic Assembly Programs in Cryptographic Primitives (Invited Talk). CONCUR (2018)
Yu-Fang Chen, Chih-Duo Hong, Ondrej Lengál, Shin-Cheng Mu, Nishant Sinha, Bow-Yaw Wang
An Executable Sequential Specification for Spark Aggregation. CoRR (2017)
Hsin-Hung Lin, Bow-Yaw Wang
Releasing VDM proof obligations with SMT solvers. MEMOCODE (2017)
Chen Luo, Fei He, Dong Yan, Dan Zhang, Xin Zhou, Bow-Yaw Wang
PSpec: a formal specification language for fine-grained control on distributed data analytics. ICSE (Companion Volume) (2017)
Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang
Certified Verification of Algebraic Properties on Low-Level Mathematical Constructs in Cryptographic Programs. CCS (2017)
Yu-Fang Chen, Chih-Duo Hong, Ondrej Lengál, Shin-Cheng Mu, Nishant Sinha, Bow-Yaw Wang
An Executable Sequential Specification for Spark Aggregation. NETYS (2017)
Fang Yu, Ching-Yuan Shueh, Chun-Han Lin, Yu-Fang Chen, Bow-Yaw Wang, Tevfik Bultan
Optimal sanitization synthesis for web application vulnerability repair. ISSTA (2016)
Fei He, Xiaowei Gao, Miaofei Wang, Bow-Yaw Wang, Lijun Zhang
Learning Weighted Assumptions for Compositional Verification of Markov Decision Processes. ACM Trans. Softw. Eng. Methodol. 25 (3) (2016)
Yu-Fang Chen, Chiao Hsieh, Ondrej Lengál, Tsung-Ju Lii, Ming-Hsien Tsai, Bow-Yaw Wang, Farn Wang
PAC learning-based verification and model synthesis. ICSE (2016)
Fei He, Shu Mao, Bow-Yaw Wang
Learning-Based Assume-Guarantee Regression Verification. CAV (1) (2016)
Yungbum Jung, Soonho Kong, Cristina David, Bow-Yaw Wang, Kwangkeun Yi
Automatically inferring loop invariants via algorithmic learning. Math. Struct. Comput. Sci. 25 (4) (2015)
Yu-Fang Chen, Chih-Duo Hong, Bow-Yaw Wang, Lijun Zhang
Counterexample-Guided Polynomial Loop Invariant Generation by Lagrange Interpolation. CAV (1) (2015)
Yu-Fang Chen, Chih-Duo Hong, Bow-Yaw Wang, Lijun Zhang
Counterexample-Guided Polynomial Loop Invariant Generation by Lagrange Interpolation. CoRR (2015)
Fei He, Xiaowei Gao, Bow-Yaw Wang, Lijun Zhang
Leveraging Weighted Automata in Compositional Reasoning about Concurrent Probabilistic Systems. POPL (2015)
Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, Bow-Yaw Wang
Commutativity of Reducers. TACAS (2015)
Yu-Fang Chen, Chiao Hsieh, Ming-Hsien Tsai, Bow-Yaw Wang, Farn Wang
CPArec: Verifying Recursive Programs via Source-to-Source Program Transformation - (Competition Contribution). TACAS (2015)
Yu-Fang Chen, Chiao Hsieh, Ondrej Lengál, Tsung-Ju Lii, Ming-Hsien Tsai, Bow-Yaw Wang, Farn Wang
PAC Learning-Based Verification and Model Synthesis. CoRR (2015)
Fei He, Bow-Yaw Wang, Liangze Yin, Lei Zhu
Symbolic assume-guarantee reasoning through BDD learning. ICSE (2014)
Yu-Fang Chen, Chang-Hong Hsu, Hsin-Hung Lin, Peter Schwabe, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang, Shang-Yi Yang
Verifying Curve25519 Software. CCS (2014)
Min Zhou, Fei He, Bow-Yaw Wang, Ming Gu, Jiaguang Sun
Array Theory of Bounded Elements and its Applications. J. Autom. Reason. 52 (4) (2014)
Yu-Fang Chen, Chiao Hsieh, Ming-Hsien Tsai, Bow-Yaw Wang, Farn Wang
Verifying Recursive Programs Using Intraprocedural Analyzers. SAS (2014)
Yu-Fang Chen, Bow-Yaw Wang, Kai-Chun Yang
Learning Summaries of Recursive Functions. APSEC (1) (2014)
Min Zhou, Fei He, Bow-Yaw Wang, Ming Gu, Jiaguang Sun
A Unified Framework for DPLL(T) + Certificates. J. Appl. Math. 2013 (2013)
Yu-Fang Chen, Bow-Yaw Wang
BULL: A Library for Learning Algorithms of Boolean Functions. TACAS (2013)
Yu-Fang Chen, Bow-Yaw Wang, Di-De Yen
A Finite Exact Representation of Register Automata Configurations. INFINITY (2013)
Fei He, Liangze Yin, Bow-Yaw Wang, Lianyi Zhang, Guanyu Mu, Wenrui Meng
VCS: A Verifier for Component-Based Systems. ATVA (2013)
Wonchan Lee, Yungbum Jung, Bow-Yaw Wang, Kwangkeun Yi
Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference Log. Methods Comput. Sci. 8 (3) (2012)
Wonchan Lee, Bow-Yaw Wang, Kwangkeun Yi
Termination Analysis with Algorithmic Learning. CAV (2012)
Yu-Fang Chen, Bow-Yaw Wang
Learning Boolean Functions Incrementally. CAV (2012)
Wenrui Meng, Fei He, Bow-Yaw Wang, Qiang Liu
Thread-Modular Model Checking with Iterative Refinement. NASA Formal Methods (2012)
Yungbum Jung, Wonchan Lee, Bow-Yaw Wang, Kwangkeun Yi
Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference. TACAS (2011)
Soonho Kong, Yungbum Jung, Cristina David, Bow-Yaw Wang, Kwangkeun Yi
Automatically Inferring Quantified Loop Invariants by Algorithmic Learning from Simple Templates. APLAS (2010)
Yu-Fang Chen, Edmund M. Clarke, Azadeh Farzan, Ming-Hsien Tsai, Yih-Kuen Tsay, Bow-Yaw Wang
Automated Assume-Guarantee Reasoning through Implicit Learning. CAV (2010)
Yungbum Jung, Soonho Kong, Bow-Yaw Wang, Kwangkeun Yi
Deriving Invariants by Algorithmic Learning, Decision Procedures, and Predicate Abstraction. VMCAI (2010)
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)
Min Zhou, Fei He, Bow-Yaw Wang, Ming Gu
On Array Theory of Bounded Elements. CAV (2010)
Geng-Dian Huang, Bow-Yaw Wang
Complete SAT-Based Model Checking for Context-Free Processes. Int. J. Found. Comput. Sci. 21 (2) (2010)
Yu-Fang Chen, Azadeh Farzan, Edmund M. Clarke, Yih-Kuen Tsay, Bow-Yaw Wang
Learning Minimal Separating DFA's for Compositional Verification. TACAS (2009)
Yih-Kuen Tsay, Bow-Yaw Wang
Automated Compositional Reasoning of Intuitionistically Closed Regular Properties. Int. J. Found. Comput. Sci. 20 (4) (2009)
Yih-Kuen Tsay, Bow-Yaw Wang
Automated Compositional Reasoning of Intuitionistically Closed Regular Properties. CIAA (2008)
Azadeh Farzan, Yu-Fang Chen, Edmund M. Clarke, Yih-Kuen Tsay, Bow-Yaw Wang
Extending Automated Compositional Verification to the Full Class of Omega-Regular Languages. TACAS (2008)
Geng-Dian Huang, Bow-Yaw Wang
Complete SAT-Based Model Checking for Context-Free Processes. ATVA (2007)
Bow-Yaw Wang
Automatic Derivation of Compositional Rules in Automated Compositional Reasoning. CONCUR (2007)
Ming-Hsien Tsai, Bow-Yaw Wang
Formalization of CTL* in Calculus of Inductive Constructions. ASIAN (2006)
Bow-Yaw Wang
Automatic Verification of a Model Checker by Reflection. PADL (2006)
Bow-Yaw Wang
On the Satisfiability of Modular Arithmetic Formulae. ATVA (2006)
Bow-Yaw Wang
Modeling and analyzing applications with domain-specific languages by reflective rewriting: a case study. SAC (2006)
Ming-Hsien Tsai, Bow-Yaw Wang
Modular Formalization of Reactive Modules in COQ. ASIAN (2006)
Fang Yu, Bow-Yaw Wang
Sat-based Model Checking for Region Automata. Int. J. Found. Comput. Sci. 17 (4) (2006)
Bow-Yaw Wang
Specification of an Infinite-State Local Model Checker in Rewriting Logic. SEKE (2005)
Bow-Yaw Wang
Proving forall-µ-Calculus Properties with SAT-Based Model Checking. FORTE (2005)
Bow-Yaw Wang
mu-Calculus Model Checking in Maude. WRLA (2004)
Farn Wang, Karsten Schmidt, Fang Yu, Geng-Dian Huang, Bow-Yaw Wang
BDD-Based Safety-Analysis of Concurrent Software with Pointer Data Structures Using Graph Automorphism Symmetry Reduction. IEEE Trans. Software Eng. 30 (6) (2004)
Fang Yu, Bow-Yaw Wang
Toward Unbounded Model Checking for Region Automata. ATVA (2004)
Fang Yu, Bow-Yaw Wang, Yao-Wen Huang
Bounded Model Checking for Region Automata. FORMATS/FTRTFT (2004)
Rajeev Alur, Bow-Yaw Wang
Verifying Network Protocol Implementations by Symbolic Refinement Checking. CAV (2001)
Rajeev Alur, Luca de Alfaro, Radu Grosu, Thomas A. Henzinger, M. Kang, Christoph M. Kirsch, Rupak Majumdar, Freddy Y. C. Mang, Bow-Yaw Wang
JMOCHA: A Model Checking Tool that Exploits Design Structure. ICSE (2001)
Bow-Yaw Wang, José Meseguer, Carl A. Gunter
Specification and Formal Analysis of a PLAN Algorithm in Maude. ICDCS Workshop on Distributed System Validation and Verification (2000)
Rajeev Alur, Radu Grosu, Bow-Yaw Wang
Automated Refinement Checking for Asynchronous Processes. FMCAD (2000)
Rajeev Alur, Bow-Yaw Wang
"Next" Heuristic for On-the-Fly Model Checking. CONCUR (1999)
Hsu-Chun Yen, Bow-Yaw Wang, Ming-Sheng Yang
Deciding a Class of Path Formulas for Conflict-Free Petri Nets. Theory Comput. Syst. 30 (5) (1997)
Hsu-Chun Yen, Bow-Yaw Wang, Ming-Sheng Yang
Some Complexity Results for Rings of Petri Nets. Int. J. Found. Comput. Sci. 5 (3/4) (1994)
Hsu-Chun Yen, Bow-Yaw Wang, Ming-Sheng Yang
A Unified Approach for Reasoning about Conflict-Free Petri Nets. Application and Theory of Petri Nets (1993)