Ruiling Chen, Jiaxiang Liu, Xiaomu Shi, Ming-Hsien Tsai, Bow-Yaw Wang, and Bo-Yin Yang. llvm2CryptoLine: Verifying Arithmetic in Cryptographic C Programs (demo). The ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE). San Francisco, USA. December 2023.
Ming-Hsien Tsai, Yu-Fu Fu, Jiaxiang Liu, Xiaomu Shi, Bow-Yaw Wang, and Bo-Yin Yang. Certified Verification for Algebraic Abstraction. 35th International Conference on Computer Aided Verification (CAV 2023). Paris, France. July 2023.
Ming-Hsien Tsai, Yu-Fu Fu, Jiaxiang Liu, Xiaomu Shi, Bow-Yaw Wang, and Bo-Yin Yang. CoqCryptoLine: A Verified Model Checker with Certified Results. 35th International Conference on Computer Aided Verification (CAV 2023). Paris, France. July 2023.
Depeng Liu, Bow-Yaw Wang, Chen Fu, and Lijun Zhang. Model Checking Differentially Private Properties. Theoretical Computer Science, 943(17), January 2023.
Vincent Hwang, Jiaxiang Liu, Gregor Seiler, Xiaomu Shi, Ming-Hsien Tsai, Bow-Yaw Wang, and Bo-Yin Yang. Verified NTT Multiplications for NISTPQC KEM Lattice Finalists: Kyber, Saber, and NTRU. Conference on Cryptographic Hardware and Embedded Systems (CHES 2022). Leuven, Belgium. September 2022.
Depeng Liu, Bow-Yaw Wang, and Lijun Zhang. Verifying Pufferfish Privacy in Hidden Markov Models. 23rd International Conference on Verification, Model Checking, and Abstraction Interpretation (VMCAI 2022). Philadelphia, USA. January 2022.
Xiaomu Shi, Yu-Fu Fu, Jiaxiang Liu, Ming-Hsien Tsai, Bow-Yaw Wang, and Bo-Yin Yang. CoqQFBV: A Scalable Certified SMT Quantifier-Free Bit-Vector Solver. 33rd International Conference on Computer-Aided Verification (CAV 2021). Virtual Conference. July 2021.
Nicky Mouha and Asmaa Hailane. The Application of Formal Methods to Real-World Cryptographic Algorithms, Protocols and Systems. IEEE Computer 54(1). January 2021 (invited panelist).
Qianshan Yu, Fei He, and Bow-Yaw Wang. Incremental Predicate Analysis for Regression Verification. The ACM SIGPLAN conference on Systems, Programming, Languages, and Applications: Software for Humanity (SPLASH)/OOPSLA. Virtual Conference. November 2020.
Rongchen Xu, Fei He, and Bow-Yaw Wang. Interval Counterexamples for Loop Invariant Learning. The ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE). Virtual Conference. November 2020.
Yu-Fu Fu, Jiaxiang Liu, Xiaomu Shi, Ming-Hsien Tsai, Bow-Yaw Wang, and Bo-Yin Yang. Signed Cryptographic Program Verification with Typed Cryptoline. 26th ACM SIGSAC Conference on Computer and Communications Security (CCS 2019). London, UK. November 2019.
Jiaxiang Liu, Xiaomu Shi, Ming-Hsien Tsai, Bow-Yaw Wang, and Bo-Yin Yang. Verifying Arithmetic in Cryptographic C Programs. 34th IEEE/ACM International Conference on Automated Software Engineering (ASE 2019). San Diego, USA. November 2019.
Yongjian Li and Bow-Yaw Wang. Parameterized Hardware Verification Through Term-Level Generalized Symbolic Trajectory Evaluation. 21st International Conference on Formal Engineering Methods (ICFEM 2019). Shenzhen, China. November 2019.
Yu-Fang Chen, Hsiao-chen Chung, Wen-Chi Hung, Ming-Hsien Tsai, Bow-Yaw Wang, and Farn Wang. Synthesize Models for Quantitative Anlysis Using Automata Learning. International Conference on Network Systems (NETYS 2019). Marrakech, Morroco. June 2019.
Depeng Liu, Bow-Yaw Wang, and Lijun Zhang. Model Checking Differentially Private Properties. 16th Asian Symposium on Programming Languages and Systems (APLAS 2018) Wellington. New Zealand, December 2018.
Andy Polyakov, Ming-Hsien Tsai, Bow-Yaw Wang, and Bo-Yin Yang. Verifying Arithmetic Assembly Programs in Cryptographic Primitives (invited). 29th International Conference on Concurrency Theory (CONCUR 2018), Beijing, China. September 2018.
Ming-Hsien Tsai, Bow-Yaw Wang, and Bo-Yin Yang. Certified Verification of Algebraic Properties on Low-Level Mathematical Constructs in Cryptographic Programs. ACM Conference on Computer and Communications Security (CCS 2017), Dallas, USA. October 2017.
Chen Luo, Fei He, Dong Yan, Dan Zhang, Xin Zhou, and Bow-Yaw Wang. PSpec: a Formal Specification Language for Fine-grained Control on Distributed Data Analytic (poster). 39th International Conference on Software Engineering (ICSE 2017), Buenos Aires, Argentina. May 2017.
Yu-Fang Chen, Chih-Duo Hong, Ondrej Lengal, Shin-Cheng Mu, Nishant Sinha,and Bow-Yaw Wang. An Executable Sequential Specification for Spark Aggregation. 5th International Conference on Networked Systems (NETYS 2017), Marrakech, Morocco. May 2017.
Fang Yu, Ching-Yuan Shueh, Chun-Han Lin, Yu-Fang Chen, Bow-Yaw Wang, and Tevfik Bultan. Optimal Sanitization Synthesis for Web Application Vulnerability Repair. The International Symposium on Software Testing and Analysis (ISSTA 2016), Saarbruecken, Germany. July 2016.
Fei He, Shu Mao, and Bow-Yaw Wang. Learning-based Assume-Guarantee Regression Verification. 28th International Conference on Computer Aided Verification (CAV 2016), Toronto, Ontario, Canada. July 2016.
Yu-Fang Chen, Chiao Hsieh, Ondrej Lengal, Tsung-Ju Lii, Ming-Hsien Tsai, Bow-Yaw Wang, and Farn Wang. PAC Learning-Based Verification and Model Synthesis. 38th International Conference on Software Engineering (ICSE 2016), Austin, USA. May 2016.
Fei He, Xiaowei Gao, Miaofei Wang, Bow-Yaw Wang, and Lijun Zhang. Learning Weighted Assumptions for Compositional Verification of Markov Decision Processes. ACM Transactions Software Engineering and Methodology (TOSEM). 25(3): 21:1-21:39 (2016).
Yu-Fang Chen, Chih-Duo Hong, Bow-Yaw Wang, and Lijun Zhang. Counterexample-Guided Polynomial Loop Invariant Generation by Lagrange Interpolation 27th International Conference on Computer Aided Verification (CAV 2015), pp 658-674, LNCS 9206. 2015.
Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang. Commutativity of Reducers. 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2015), pp 131-146, LNCS 9035. 2015.
Fei He, Xiaowei Gao, Bow-Yaw Wang, and Lijun Zhang. Leveraging Weighted Automata in Compositional Reasoning about Concurrent Probabilistic Systems. 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2015), pp 503-514. 2015.
Yungbum Jung, Soonho Kong, Cristina David, Bow-Yaw Wang, and Kwangkeun Yi. Automatically inferring loop invariants via algorithmic learning. Mathematical Structures in Computer Science 25(4): 892-915 (2015).
Yu-Fang Chen, Bow-Yaw Wang and Kai-Chun Yang. Learning Summaries of Recursive Functions. 21st Asia-Pacific Software Engineering Conference (APSEC 2014), Jeju, South Korea. December 1 - 4, 2014.
Yu-Fang Chen, Chang-Hong Hsu, Hsin-Hung Lin, Peter Schwabe, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang, and Shang-Yi Yang. Verifying Curve25519 Software. 21st ACM Conference on Computer and Communications Security (CCS 2014), pp 299-309. 2014.
Yu-Fang Chen, Chiao Hsieh, Ming-Hsien Tsai, Bow-Yaw Wang, and Farn Wang. Verifying Recursive Programs Using Intraprocedural Analyzers. 21st International Symposium on Static Analysis (SAS 2014), pp 118-133, LNCS 8723. 2014.
Fei He, Bow-Yaw Wang, Liangze Yin, and Lei Zhu. Symbolic Assume-Guarantee Reasoning through BDD Learning. 36th International Conference on Software Engineering (ICSE 2014), pp 1071-1082. 2014.
Min Zhou, Fei He, Bow-Yaw Wang, Ming Gu, and Jiaguang Sun. Array Theory of Bounded Elements and its Applications. Journal of Automated Reasoning. 52(4): 379-405 (2014).
Fei He, Liangze Yin, Bow-Yaw Wang, Lianyi Zhang, Guanyu Mu, Wenrui Meng. VCS: A Verifier for Component-Based Systems. Automated Technology for Verification and Analysis (ATVA 2013), pp 478-481, LNCS 8172. 2013.
Min Zhou, Fei He, Bow-Yaw Wang, Ming Gu, Jiaguang Sun. A Unified Framework for DPLL(T) + Certificates. Journal of Applied Mathematics, (2013). 2013.
Yu-Fang Chen and Bow-Yaw Wang. BULL: A Library for Learning Algorithms of Boolean Functions. 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems . Rome, Italy. March, 2013.
Wonchan Lee, Yungbum Jung, Bow-Yaw Wang, Kwangkuen Yi. Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference. Logical Methods in Computer Science 8(3), 2012.
Yu-Fang Chen and Bow-Yaw Wang. Learning Boolean Functions Incrementally. 24th International Conference on Computer Aided Verification (CAV '12) . Berkeley, USA. July 7-13, 2012.
Wonchan Lee, Bow-Yaw Wang, and Kwangkeun Yi. Termination Analysis with Algorithmic Learning. 24th International Conference on Computer Aided Verification (CAV '12) . Berkeley, USA. July 7 - 13, 2012.
Wenrui Meng, Fei He, Bow-Yaw Wang, and Qiang Liu. Thread-Modular Model Checking with Iterative Refinement. 4 th NASA Formal Methods (NFM '12) . Norfolk, USA. April 3-5, 2012.
Yungbum Jung, Wonchan Lee, Bow-Yaw Wang, and Kwangkeun Yi. Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference. 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '11). Saarbruecken, Germany. March 28 - 31, 2011.
Soonho Kong, Yungbum Jung, Cristina David, Bow-Yaw Wang, and Kwangkeun Yi. Automatically Inferring Quantified Loop Invariants by Algorithmic Learning from Simple Templates. 8th Asian Symposium on Programming Languages and Systems (APLAS '10). Shanghai, China. November 28 - December 1, 2010.
Yu-Fang Chen, Edmund M. Clarke, Azadeh Farzan, Fei He, Ming-Hsien Tsai, Yih-Kuen Tsay, Bow-Yaw Wang, and Lei Zhu. Comparing Learning Algorithms in Automated Assume-Guarantee Reasoning. 4th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISOLA '10). Crete, Greece. 18 - 20 October, 2010.
Yu-Fang Chen, Edmund M. Clarke, Azadeh Farzan, Ming-Hsien Tsai, Yih-Kuen Tsay, and Bow-Yaw Wang. Automated Assume-Guarantee Reasoning through Implicit Learning. 22nd International Conference on Computer Aided Verification (CAV '10). Edinburgh, UK. July 15 - July 19, 2010.
Min Zhou, Fei He, Bow-Yaw Wang, and Ming Gu. On Array Theory of Bounded Elements. 22nd International Conference on Computer Aided Verification (CAV '10). Edinburgh, UK. July 15 - July 19, 2010.
Yungbum Jung, Soonho Kong, Bow-Yaw Wang, and Kwangkeun Yi. Deriving Invariants by Algorithmic Learning, Decision Procedures, and Predicate Abstraction. 11th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI '10). Madrid, Spain. January 17 - January 19, 2010.
Geng-Dian Huang, Bow-Yaw Wang. Complete SAT-Based Model Checking for Context-Free Processes. International Journal of Foundations of Computer Science. 21(2): 115-134 (2010).
Yu-Fang Chen, Azadeh Farzan, Edmund M. Clarke, Yih-Kuen Tsay, and Bow-Yaw Wang. Learning Minimal Separating DFA's for Compositional Verification. 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '09). York, UK. March 23 - March 26, 2009.
Yih-Kuen Tsay, Bow-Yaw Wang. Automated Compositional Reasoning of Intuitionistically Closed Regular Properties. International Journal of Foundations of Computer Science. 20(4): 747-762 (2009).
Yih-Kuen Tsay and Bow-Yaw Wang. Automated Compositional Reasoning of Intuitionistically Closed Regular Properties . 13th International Conference on Implementation and Application of Autoamta (CIAA '08). San Francisco, USA. July 21-24, 2008.
Azadeh Farzon, Yu-Fang Chen, Edmund M. Clarke, Yih-Kuen Tsay, and Bow-Yaw Wang. Extending Automated Compositional Verification to the Full Class of Omega-Regular Languages. 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '08). Budapest, Hungary. March 29 - April 6, 2008.
Geng-Dian Huang and Bow-Yaw Wang. Complete SAT-based Model Checking for Context-Free Processes. 5th International Symposium on Automated Technology for Verification and Analysis (ATVA '07). Tokyo, Japan. October 22-25, 2007.
Bow-Yaw Wang. Automatic Derivation of Compositional Rules in Automated Compositional Reasoning. 18th International Conference on Concurrency Theory (CONCUR '07). Lisbon, Portugal. September 3-8, 2007.
Ming-Hsien Tasi and Bow-Yaw Wang. Modular Formalization of Reactive Modules in Coq. 11th Annual Asian Computing Science Conference (ASIAN '06). Tokyo, Japan. December 6-8, 2006.
Ming-Hsien Tasi and Bow-Yaw Wang. Formalization of CTL* in the Calculus of Inductive Constructions. 11th Annual Asian Computing Science Conference (ASIAN '06). Tokyo, Japan. December 6-8, 2006.
Bow-Yaw Wang. On the Satisfiability of Modular Arithmetic Formulae. 4th Automated Technology for Verification and Analysis. Beijing, China. October 2006.
Bow-Yaw Wang. Modeling and Analyzing Applications with Domain-Specific Languages by Reflective Rewriting: a Case Study. 21st ACM Symposium on Applied Computing. Dijon, France. April 23-27, 2006.
Bow-Yaw Wang. Automatic Verification of a Model Checker by Reflection. Eighth International Symposium on Practical Aspects of Declarative Languages. Charleston, South Carolina, USA. January 9-10, 2006.
Bow-Yaw Wang. Proving \forall\mu-Calculus Properties with SAT-Based Model Checking. 25th IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems. Taipei, Taiwan. October 2-5, 2005.
Bow-Yaw Wang. Automatic Verification of a Model Checker in Rewriting Logic. Technical Report TR-IIS-05-009. Institute of Information Science, Academia Sinica. 2005.
Bow-Yaw Wang. Specification of an Infinite-State Local Model Checker in Rewriting Logic. The Seventeenth International Conference on Software Engineering and Knowledge Engineering. Taipei, Taiwan. July 14-16, 2005.
Bow-Yaw Wang. Proving \forall\mu-Calculus Properties with SAT-Based Model Checking. Technical Report TR-IIS-05-003. Institute of Information Science, Academia Sinica, 2005.
Fang Yu and Bow-Yaw Wang. Toward Unbounded Model Checking for Region Automata. 2nd International Symposium on Automated Technology for Verification and Analysis. Taipei, Taiwan. November 2004.
Fang Yu, Bow-Yaw Wang, and Yao-Wen Huang. Bounded Model Checking for Region Automata. Joint International Conferences on Formal Modelling and Analysis of Timed Systems (FORMATS) and Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT). Grenoble, France. September 2004.
F. Wang, K. Schmidt, F. Yu, G.D. Huang, and B.-Y. Wang. BDD-Based Safety-Analysis of Concurrent Software with Pointer Data Structures Using Graph Automorphism Symmetry Reduction. IEEE Transactions on Software Engineering, 30(6), June 2004.
Bow-Yaw Wang. Mu-Calculus Model Checking in Maude. 5th International Workshop on Rewriting Logic and Its Applications (WRLA '04). Barcelona, Spain. March 27-28, 2004.
R. Alur, L. de Alfaro, R. Grosu, T.A. Henzinger, M. Kang, R. Majumdar, F. Mang, C.M. Kirsch, and B.-Y. Wang. Mocha: A Model Checking Tool that Exploits Design Structure. 23rd International Conference on Software Engineering. pp. 835--836, 2001.
Rajeev Alur and Bow-Yaw Wang. Verifying Network Protocol Implementations by Symbolic Refinement Checking. Computer Aided Verification (CAV '01). Paris, France. July 18-23, 2001.
Rajeev Alur, Grosu Radu and Bow-Yaw Wang. Automated Refinement Checking for Asynchronous Processes. Formal Methods in Computer Aided Design (FMCAD00). Austin, Texas. November 1-3, 2000.
Bow-Yaw Wang, Jose Meseguer, and Carl A. Gunter. Specification and formal verification of a PLAN algorithm in Maude. Proceedings of the 2000 ICDCS workshop on Distributed System Validation and Verification, IEEE Computer Society. April 2000.
Rajeev Alur and Bow-Yaw Wang. ``Next'' Heuristic for On-the-fly Model Checking. CONCUR '99: Concurrency Theory, Tenth International Conference, LNCS 1664. 98-113, 1999.
Hsu-Chun Yen, Bow-Yaw Wang, and Ming-Sheng Yang. Deciding a Class of Path Formulas for Conflict-Free Petri Nets. Theory of Computing Systems. 30(5): 475-494 (1997).
Hsu-Chun Yen, Bow-Yaw Wang, and Ming-Sheng Yang. Some Complexity Results for Rings of Petri Nets. International Journal of Foundations of Computer Science. Vol. 5 No. 3&4, 1994, pp. 281-292.