Bow-Yaw Wang's Publications </head> <body> <h2>Bow-Yaw Wang's Publications</h2> <hr>  <p> Adadeh Farzon, Yu-Fang Chen, Edmund M. Clarke, Yih-Kuen Tsay, and Bow-Yaw Wang. <a href="http://www.iis.sinica.edu.tw/~bywang/papers/tacas08.pdf.gz"> Extending Automated Compositional Verification to the Full Class of Omega-Regular Languages</a>. <i>14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '08)</i>. Budapest, Hungary. March 29 - April 6, 2008. <p> Geng-Dian Huang and Bow-Yaw Wang. <a href="http://www.iis.sinica.edu.tw/~bywang/papers/atva07.pdf.gz"> Complete SAT-based Model Checking for Context-Free Processes</a>. <i>5th International Symposium on Automated Technology for Verification and Analysis (ATVA '07)</i>. Tokyo, Japan. October 22-25, 2007. <p>Bow-Yaw Wang. <a href="http://www.iis.sinica.edu.tw/~bywang/papers/concur07.pdf.gz"> Automatic Derivation of Compositional Rules in Automated Compositional Reasoning</a>. <i>18th International Conference on Concurrency Theory (CONCUR '07)</i>. Lisbon, Portugal. September 3-8, 2007. <p> Ming-Hsien Tasi and Bow-Yaw Wang. <a href="http://www.iis.sinica.edu.tw/~bywang/papers/asian-0.pdf.gz"> Modular Formalization of Reactive Modules in Coq</a>. <i>11th Annual Asian Computing Science Conference (ASIAN '06)</i>. Tokyo, Japan. December 6-8, 2006. <p> Ming-Hsien Tasi and Bow-Yaw Wang. <a href="http://www.iis.sinica.edu.tw/~bywang/papers/asian-1.pdf.gz"> Formalization of CTL* in the Calculus of Inductive Constructions</a>. <i>11th Annual Asian Computing Science Conference (ASIAN '06)</i>. Tokyo, Japan. December 6-8, 2006. <p> Bow-Yaw Wang. <a href="http://www.iis.sinica.edu.tw/~bywang/papers/atva06.pdf.gz"> On the Satisfiability of Modular Arithmetic Formulae</a>. <i>4th Automated Technology for Verification and Analysis</i>. Beijing, China. October 2006. <p> Bow-Yaw Wang. <a href="http://www.iis.sinica.edu.tw/~bywang/papers/sac06.pdf.gz"> Modeling and Analyzing Applications with Domain-Specific Languages by Reflective Rewriting: a Case Study</a>. <i>21st ACM Symposium on Applied Computing</i>. Dijon, France. April 23-27, 2006. <p> Bow-Yaw Wang. <a href="http://www.iis.sinica.edu.tw/~bywang/papers/padl06.pdf.gz"> Automatic Verification of a Model Checker by Reflection</a>. <i>Eighth International Symposium on Practical Aspects of Declarative Languages</i>. Charleston, South Carolina, USA. January 9-10, 2006. <p> Bow-Yaw Wang. <a href="http://www.iis.sinica.edu.tw/~bywang/papers/forte05.pdf.gz"> Proving \forall\mu-Calculus Properties with SAT-Based Model Checking</a>. <i>25th IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems</i>. Taipei, Taiwan. October 2-5, 2005. <p> Bow-Yaw Wang. <a href="http://www.iis.sinica.edu.tw/LIB/TechReport/tr2005/tr05009.pdf"> Automatic Verification of a Model Checker in Rewriting Logic</a>. <i>Technical Report TR-IIS-05-009</i>. Institute of Information Science, Academia Sinica. 2005. <p> Bow-Yaw Wang. <a href="http://www.iis.sinica.edu.tw/~bywang/papers/seke05.pdf.gz"> Specification of an Infinite-State Local Model Checker in Rewriting Logic</a>. <i>The Seventeenth International Conference on Software Engineering and Knowledge Engineering</i>. Taipei, Taiwan. July 14-16, 2005. <p> Bow-Yaw Wang. <a href="http://www.iis.sinica.edu.tw/LIB/TechReport/tr2005/tr05003.pdf"> Proving \forall\mu-Calculus Properties with SAT-Based Model Checking</a>. <i>Technical Report TR-IIS-05-003</i>. Institute of Information Science, Academia Sinica, 2005. <p> Fang Yu and Bow-Yaw Wang. <a href="http://www.iis.sinica.edu.tw/~bywang/papers/atva04.pdf.gz"> Toward Unbounded Model Checking for Region Automata</a>. <i>2nd International Symposium on Automated Technology for Verification and Analysis</i>. Taipei, Taiwan. November 2004. <p> Fang Yu, Bow-Yaw Wang, and Yao-Wen Huang. <a href="http://www.iis.sinica.edu.tw/~bywang/papers/formats04.pdf.gz"> Bounded Model Checking for Region Automata</a>. <i>Joint International Conferences on Formal Modelling and Analysis of Timed Systems (FORMATS) and Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT)</i>. Grenoble, France. September 2004. <p> 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. <p> Bow-Yaw Wang. <a href="http://www.iis.sinica.edu.tw/~bywang/papers/wrla04.pdf.gz"> Mu-Calculus Model Checking in Maude</a>. <i>5th International Workshop on Rewriting Logic and Its Applications (WRLA '04)</i>. Barcelona, Spain. March 27-28, 2004. <p> R. Alur, L. de Alfaro, R. Grosu, T.A. Henzinger, M. Kang, R. Majumdar, F. Mang, C.M. Kirsch, and B.-Y. Wang. <a href="http://www.iis.sinica.edu.tw/~bywang/papers/icse01.pdf.gz"> Mocha: A model checking tool that exploits design structure</a>, <i>23rd International Conference on Software Engineering</i>. pp. 835--836, 2001. <p> Rajeev Alur and Bow-Yaw Wang. <a href="http://www.iis.sinica.edu.tw/~bywang/papers/cav.ps.gz"> Verifying Network Protocol Implementations by Symbolic Refinement Checking</a>. <i>Computer Aided Verification (CAV '01)</i>. Paris, France. July 18-23, 2001. <p> Rajeev Alur, Grosu Radu and Bow-Yaw Wang. <a href="http://www.iis.sinica.edu.tw/~bywang/papers/fmcad00.ps.gz"> Automated Refinement Checking for Asynchronous Processes</a>. <i>Formal Methods in Computer Aided Design (FMCAD00)</i>. Austin, Texas. November 1-3, 2000. <p> Bow-Yaw Wang, Jose Meseguer, and Carl A. Gunter. <A HREF="http://www.iis.sinica.edu.tw/~bywang/papers/dsvv-00.ps.gz"> Specification and formal verification of a PLAN algorithm in Maude.</A>. <I>Proceedings of the 2000 ICDCS workshop on Distributed System Validation and Verification, IEEE Computer Society</I>. April 2000. <p> Rajeev Alur and Bow-Yaw Wang. <a href="http://www.iis.sinica.edu.tw/~bywang/papers/concur99.ps.gz"> ``Next'' Heuristic for On-the-fly Model Checking</a>. <I>CONCUR '99: Concurrency Theory, Tenth International Conference, LNCS 1664</i>. 98-113, 1999. <p> Hsu-Chun Yen, Bow-Yaw Wang, and Ming-Sheng Yang. <A HREF="http://www.iis.sinica.edu.tw/~bywang/papers/cff.ps.gz"> Deciding a Class of Path Formulas for Conflict-Free Petri Nets</A>. <I>Theory of Computing Systems</I>. 30(5):475-494, September/October 1997. <p> Hsu-Chun Yen, Bow-Yaw Wang, and Ming-Sheng Yang. <A HREF="http://www.iis.sinica.edu.tw/~bywang/papers/ring.ps.gz"> Some Complexity Results for Rings of Petri Nets.</A>. <i>International Journal of Foundations of Computer Science</i>. Vol. 5 No. 3&4, 1994, pp. 281-292. <hr> <h3>Doctoral Dissertation:</h3> <a href="http://www.cis.upenn.edu/~bywang/thesis.html"> Hierarchical Reduction and Refinement Checking for Asynchronous Processes</a>. December 2001