Selected Publications

I. Journal articles

  1. C.-H. Huang, Schewe, F. Wang (corresponding author).  Model-Checking Iterated Games, Acta Informatica, ISSN 0001-5903, DOI 10.1007/s00236-016-0277-y. 
  2. C.-H. Huang, D. A. Peled, S. Schewe, F. Wang (corresponding author).  A Game-Theoretic Foundation for the Maximum Software Resilience against Dense Errors, to appear in IEEE Transactions on Software Engineering (TSE), Vol. 42, Issue 7, July 2016, pp.605-622. 
  3. F. Wang, S. Schewe, C.-H. Huang.  An Extension of ATL with Strategy Interaction.  ACM Transactions on Programming Languages and Systems (TOPLAS), Vol. 37, Issue 3, June 2015, ACM New York, NY, USA.
  4. F. Wang, S. Schewe, J.-H. Wu.  Complexity of Node Coverage Games. Theoretical Computer Science (TCS), Vol. 576, 20 April 2015, Pages 45–60, Elsevier.
  5. F. Wang.  Model-Checking Distributed Real-Time Systems with Propositions, Events, and Fairness Assumptions.  To be archived in International Journal on Software Tools for Technology Transfer (STTT), Jan. 2014, Springer-Verlag. 
  6. F. Wang.  Efficient Model-Checking of Dense-Time Systems with Time-Convexity Analysis.  Theoretical Computer Science (TCS), Elsevier, Jan. 2013. 
  7. F. Wang, L.-W. Yao, Y.-L. Yang.  Efficient Verification of Distributed Real-Time Systems
    with Broadcasting Behaviors.      Real-Time Systems     Journal, Vol. 47, Nr. 4, pp 285-318,     July 2011. 
  8. F. Wang.  Specification Formalisms and Models. Wiley Encyclopedia of Computer Science and Engineering 2008. 
  9. F. Wang, G.-D. Huang, F. Yu.  TCTL Inevitability Analysis of Dense-Time Systems: From Theory to Engineering.  IEEE Transactions on Software Engineering, Vol. 32, Nr. 7, July 2006, IEEE Computer Society. 
  10. F. Wang.  Symbolic Parametric Safety Analysis of Linear Hybrid Systems with BDD-like Data-Structures.  IEEE Transactions on Software Engineering, Volume 31,  Issue 1  (January 2005), pp. 38-51, IEEE Computer Society. 
  11. F. Wang.  Inductive Composition of Numbers with Maximum, Minimum, and Addition - A New Theory for Program Execution-Time Analysis.  International Journal of Foundations of Computer Science, Vol. 15, Nr. 6, Dec. 2004, World  Scientific. 
  12. F. Wang, H.-C. Yen.  Reachability Solution Characterization of Parametric Real-Time Systems.  Theoretical Computer Science 328 (2004), pp.187-201, Elsevier, special issue for CIAA 2003. 
  13. F. Wang.  Formal Verification of Timed Systems: A Survey and Perspective.   Proceedings of the IEEE, Vol. 92, Nr. 8, August 2004, pp.1283-1307, IEEE. 
  14. F. Wang, K. Schmidt, G.-D. Huang, F. Yu, B.-Y. Wang.  BDD-based Safety Analysis of Concurrent Software with Pointer Data Structures using Graph Automorphism Symmetry Reduction. IEEE Transactions on Software Engineering, Vol. 30, Nr. 6, June 2004, ISSN 0098-5589, pp.403-417, IEEE. 
  15. F. Wang.  Efficient Verification of Timed Automata with BDD-like Data-Structures. International Journal on Software Tools for Technology Transfer (STTT), Vol. 6, Nr. 1, July 2004, Springer-Verlag, special issue for the 4th International Conference on Verification, Model-Checking, and Abstract Interpretation (VMCAI’2003), New York City, USA, January 2003.
  16. F. Wang, G.-D. Huang, F. Yu.  Symbolic Simulation of Industrial Real-Time and Embeded Systems - Experiments with the Bluetooth baseband communication ptotocol, invited to the first issue of the journal of Embedded Computing (JEC), Vol. 1, Issue 1, Cambridge International Science Publishing. 
  17. F. Wang, P.-A. Hsiung.  Efficient and User-Friendly Verification.  IEEE Transactions on Computers 51(1), Jan. 2002, ISSN 0018-9340, pp.61-84. 
  18. F. Wang.  Parametric Analysis of Computer Systems. Journal of Formal Methods in Systems Design 17, 2000, pp.39-60, Kluwer Academic Publishers.
  19. F. Wang, C.-T. Lo.  Procedure-Level verification of Real-Time Concurrent Systems. the Journal of Real-Time Systems, vol. 16, Nr. 1, January 1999, pp.81-114, Kluwer Academic Publishers.
  20. J. Yang, A.K. Mok, F. Wang.  Symbolic Model Checking for Event-Driven Real-Time Systems. ACM Transactions on Programming Languages and Systems, Vol. 19, Nr. 2, March 1997, pages 386-412. (with J. Yang, A.K. Mok)
  21. F. Wang.  A Temporal Logic for Real-Time Partial-Ordering with Named Transactions. Theoretical Computer Science, Vol. 181, Nr. 1, 15 July 1997, pp. 195-225; Guest Editor : R. Baeza Yates, E. Coles. A preliminary version also appears in Proceedings of Latin American Theoretical INformatics Symposium, Santiago, Chile, April, 1995. LNCS 911, Springer-Verlag.
  22. F. Wang.  Parametric Timing Analysis of Real-Time Systems. Information and Computation, Vol. 130, Nr 2, Academic Press, ISSN 0890-5401, Nov. 1996; pp.131-150.
  23. F. Wang, A.K. Mok, E.A. Emerson.  Real-Time Distributed System Specification and Verification in APTL. ACM Transactions on Software Engineering and Methodology, Vol. 2, No. 4, Octobor 1993, pp. 346-378.

II. Conference and workshop articles

  1. Wei Ji, Farn Wang, Peng Wu, Yi Lv.  An Experiment on Decision Diagrams for Model Checking Probabilistic Timed Automata.  Proceedings of the 21st International Conference on Engineering of Complex Computer Systems (ICECCS), Nov. 2016, Dubai, UAE. 

  2. 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.  ACM/IEEE International Conference on Software Engineering (ICSE), 2016, pp.714-724.

  3. 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).  Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2015, LNCS 9035, Springer-Verlag, pp.426-428

  4. Yu-Fang Chen, Chiao Hsieh, Ming-Hsien Tsai, Bow-Yaw Wang, Farn Wang.  Verifying Recursive Programs Using Intraprocedural Analyzers.  Static Analysis Symposium (SAS), 2014,  LNCS 8723, Springer-Verlag, pp.118-133. 

  5. F. Wang, J.H. Wu, C.-H. Huang, C.-C. Chang, C.C. Li.  Temporal Specification Mining for Anomaly Analysis.  APLAS (Asian Symposium on Programming Language and Systems), Melbourne, Australia, Dec. 2013, LNCS 8301, Springer-Verlag. 

  6. C.-H. Huang, S. Schewe, F. Wang. Model-Checking Iterative Games. TACAS (Tools and Algorithms for Construction and Analysis of Systems) 2013, Rome, LNCS 7795, Springer-Verlag.

  7. C.-H. Huang, D.A. Peled, S. Schewe, and F. Wang.  Rapid Recovery for Systems with Scarce Faults.  3rd International Symposium on Games, Automata, Logics, and Formal Verification (GANDALF), September 2012. 

  8. F. Yu, S.-C. Yang, F. Wang, G.-C. Chen, and C.-C. Chan.  Symbolic Consistency Checking of OpenMP Parallel Programs.  SIGPLAN/SIGBED Conference on Languages, Compilers, and Tools for Embedded Systems (LCTES), June, 2012, Beijing.

  9. F. Wang,  L.-W. Yao,  J.-H. Wu.  Intelligent Test Oracle Construction for Reactive Systems without Explicit Specifications.  9th IEEE International Conference on Dependable, Autonomic and Secure Computing (DASC), Sydney, Australia.  Dec. 12-14, 2011.  IEEE Computer Society. 

  10. F. Wang, Y.-L. Yang, S.-C. Yang.  Regression Testing Based on Neural Networks and Program Slicing Techniques.  International Conference on Intelligent Systems and Knowledge Engineering (ISKE), Dec. 2011, Springer-Verlag.    

  11. F. Wang, J.-C. Wu, Y.-C. Lee, L.-W. Yao.  Regression Testing of Bug-fixes with AI Techniques.  International Conference on Intelligent Systems and Knowledge Engineering (ISKE), Dec. 2011, Springer-Verlag.   
  12. F. Wang, C.-H. Huang, F. Yu.   A Temporal Logic for the Interaction of Strategies.  22nd CONCUR (Concurrency Theory), Sept. 2011, Aachen.  LNCS 6901, Springer-Verlag.
  13. F. Wang, J.-H. Wu, C.-H. Huang.  Evolving a Test Oracle in Black-Box Texting.   ETAPS FASE (Fundamental Approaches to Software Engineering), April 2011, Saarbrucken.  LNCS 6603, Springer-Verlag. 
  14. Farn Wang.  Lazy Decision Diagrams for Word-Level Model Manipulation in Software Verification. IEEE TASE (Theoretical Aspects of Software Engineering), Oct. 2010.  pp 183-186.  IEEE Computer Society. 
  15. G.-D. Huang, L.-Z. Cai, F. Wang.  LTL Model Checking for Recursive Programs.  ATVA 2009: 382-396, LNCS, Springer-Verlag. 
  16. J.-H. Wu, Y.-C. Chen, S.-H. Hsieh, H.-C. Lin, Y.-Y. Chen, P.-H. Cheng, F. Wang, F. Lai.  Real-time Automated MDRO Surveillance System.  BIOCOMP 2009: 764-769
  17. Farn Wang.  Symbolic Branching Bisimulation-Checking of Dense-Time Systems in an Environment. HSCC (Hybrid System Control & Computation), 2009, pp 485-489. 
  18. F. Wang.  Efficient Model-Checking of Dense-Time Systems with Time-Convexity Analysis.  RTSS 2008, Dec. 2008, Barcelona.  IEEE Computer Society. 
  19. F. Wang.  Time-Progress Evaluation for Dense-Time Automata with Concave Path Conditions.  ATVA 2008, Oct. 2008, Seoul.  LNCS, Springer-Verlag. 
  20. F. Wang, Geng-Dian Huang.  Test Plan Generation for Concurrent Real-Time Systems based on Zone Coverage Analysis.  TESTCOM/FATES 2008, June 2008, Tokyo.  LNCS 5047, Springer-Verlag.  [PPT file]
  21. F. Wang, Chih-Hong Cheng.  Program Repair Suggestions from Graphical State-Transition Specifications.   FORTE 2008, June 2008, Tokyo.  LNCS 5048, Springer-Verlag. [PPT file]
  22. F. Wang.  Symbolic Simulation Checking of Dense-Time Automata.  5th FORMATS (International Conference on Formal Modelling and Analysis of Timed Systems.  Oct, 2007, Salzburg, Austria.  LNCS 4763, Springer-Verlag.  [PPT file]
  23. F. Wang.  Symbolic Verification of Distributed Real-Time Systems with Complex Synchronizations.  7th ICFEM (International Conference on Formal Engineering Methods), Nov. 2005, Manchester, UK.   LNCS, Springer-Verlag.  [PPT file]
  24. G.-D. Huang, F. Wang.  Automatic Test Case Generation with Region-Related Coverage Annotations for Real-Time Systems.  3rd ATVA (Automated Technology for Verification and Analysis), Oct. 2005, Taipei.  LNCS 3707, Springer-Verlag.   
  25. F. Wang, R.-S. Wu, G.-D. Huang.  Verifying Timed and Linear Hybrid Rule-Systems with RED.  17th SEKE (International Conference on Software Engineering and Knowledge Engineering), July 14-16, 2005,Taipei. 
  26. L.-Z. Cai, F. Wang, H.-C. Yen, C.-L. Lei, S.-D. Wang.  Designing and Developing a Formal Method Course of Software Engineering.  1st Taiwan Software Engineering Conference, June 3-4, 2005, Taipei. 
  27. F. Wang.   Symbolic Parametric Safety Analysis of Linear Hybrid Systems with BDD-like Data-Structures.  CAV 2004, LNCS 3114, Springer-Verlag; Boston, USA, July 2004. 
  28. F. Wang.  Model-Checking Distributed Real-Time Systems with States, Events, and Multiple Fairness Assumptions.   AMAST 2004, LNCS 3116, Springer-Verlga; Stirling, UK, July 2004. 
  29. F. Wang, G.-D. Huang, F. Yu.  Numerical Coverage Estimation for the Symbolic Simulation of Real-Time Systems.  FORTE'2003, LNCS 2767, Springer-Verlag; Berlin, Sept.-Oct. 2003.
  30. F. Wang, G.-D. Huang, F. Yu.  TCTL Inevitability Analysis of Dense-Time Systems, in proceedings of the 8th International Conference on Implementation and Application of Automata (CIAA), LNCS 2759, Springer-Verlag, July 2003, Santa Barbara, CA, USA. 
  31. F. Wang, H.-C. Yen.  Timing Parameter Characterization of Real-Time Systems. 8th International Conference on Implementation and Application of Automata (CIAA), LNCS 2759, Springer-Verlag, July 2003, Santa Barbara, CA, USA. 
  32. F. Wang, G.-D. Huang, F. Yu.  Symbolic Simulation of Real-Time Concurrent Systems. RTCSA’2003, LNCS 2968, Springer-Verlag.  
  33. F. Wang.  Efficient Verification of Timed Automata with BDD-like Data-Structures.  Proceedings of the 4th VMCAI (Verification, Model-Checking, and Abstract-Interpretation), LNCS 2575, Springer-Verlag, Jan. 2003. 
  34. F. Wang, K. Schmidt.  Symmetric Symbolic Safety-Analysis of Concurrent Software with Pointer Data Structures.  Proceedings of IFIP FORTE, LNCS 2529, Springer-Verlag; November 2002, Houston, U.S.A.
  35. F. Wang.  Symmetric Model-Checking of Concurrent Timed Automata with Clock-Restriction Diagram, RTCSA’2002, March 18-20, 2002, Tokyo, Japan.
  36. F. Wang.  RED: Model-Checker for Timed Automata with Clock-Restriction Diagram.  In proceedings of Workshop on Real-Time Tools, Aalborg University, Denmark, August 20, 2001.  Technical Report 2001-014, ISSN 1404-3203, Department of Information Technology, Uppsala University.  
  37. F. Wang.  Symbolic Verification of Complex Real-Time Systems with Clock-Restriction Diagram.  FORTE 2001(the 21st International Conference on Formal Techniques for Networked and Distributed Systems), Cheju Island, Korea.  25-28 Aug, 2001.  
  38. F. Wang, H.-C. Yen.  Parametric Optimization of Open Real-Time Systems.  SAS 2001 (Static Analysis Symposium), Paris, France, 16-18 July, 2001; LNCS 2126, Springer-Verlag. 
  39. F. Wang.  Region Encoding Diagram for Fully Symbolic Verification of Real-Time Systems.  24'th COMPSAC'2000 (Computer Software and Applications Conference), Oct, 2000.
  40. F. Wang.  Efficient Data Structure for Fully Symbolic Verification of Real-Time Software Systems.  TACAS'2000, LNCS 1785, Springer-Verlag.
  41. P.-A. Hsiung, Y.-S. Kuo, F. Wang.  Verification of Concurrent Client-Server Real-Time Scheduling Systems.  RTCSA'99, Dec., 1999, IEEE press.
  42. P.-A. Hsiung, F. Wang.  User-Friendly Verification.  FORTE/PSTV'99 (FORmal description TEchnique/Protocol Specification, Testing, Verification), October, 1999. 
  43. F. Wang.  Automatic Verification of Pointer Data-Structure Systems for All Numbers of Processes.  FM'99 (Formal Method World Congress), September 1999, LNCS 1708, Springer-Verlag.
  44. P.-A. Hsiung, Y.-S. Kuo, F. Wang.  Scheduling System Verification.  TACAS 1999(Tools and Algorithms for the Construction and Analysis of Systems), March 1999, LNCS 1579, Springer-Verlag.
  45. P.-A. Hsiung, F. Wang.  A State Graph Manipulator Tool for Real-Time System Specification and Verification. 1998 RTCSA (Real-Time Computing Systems and Applications) Workshop, October 1998, Hiroshima, Japan.
  46. F. Wang, P.-A. Hsiung.  Automatic Verification on the Large. Invited for presentation in 1998 IEEE HASE (High-Assurance Systems Engineering) Symposium, Nov. 13-14, Washington, D.C., USA.
  47. F. Wang, P.-A. Hsiung.  Parametric Analysis of Computer Systems.  In Proceedings of the 6th AMAST (Algebraic Methodology And Software Technology) Conference, Sydney, Australia, December, 1997; LNCS 1349, Springer-Verlag. (with P.-A. Hsiung)
  48. T.-W. Kuo, F. Wang, S.-J. Ho, J.-H. Wey.  PASS: A Prototyping, Analysis, Simulation, and Synthesis Environment for Real-Time Systems. to appear in Proceedings of the 4th RTCSA (Real-Time Computing Systems and Applications), Taipei, Taiwan, October, 1997
  49. T.-W. Kuo, F. Wang, D. Locke.  Error Propagation Analysis of Real-Time Data-Intensive Applications. work-in-progress paper, in Proceedings of the 3rd IEEE RTAS (Real-Time Technology and Applications Symposium), Montreal, Canada, June, 1997.
  50. F. Wang.  High-Level Execution Time Analysis. in Proceedings of the Fourth International AMAST Worshop on Real-Time Systems, Concurrent, and Distributed Software (ARTS'97), Mallorca, Spain, May, 1997; LNCS 1231, Springer-Verlag.
  51. F. Wang.  Scalable Compositional Verification of High-Level Real-Time Concurrent Systems : From 10^7 to 10^{85} states.  In Proceedings of the 3rd RTCSA (Real-Time Computing Systems and Applications), Seoul, Korea, October, 1996
  52. F. Wang.  Scalable Compositional Reachability Analysis of Real-Time Concurrent Systems. In Proceedings of the 2nd IEEE RTAS (Real-Time Technology and Applications Symposium), Boston, June, 1996.
  53. F. Wang, C.-T. Lo.  Procedure-Level Verification of Real-time Concurrent Systems. In Proceedings of the 3rd FME (Formal Method Europe) Symposium, Oxford, England, March, 1996; LNCS 1051, Springer-Verlag.
  54. F. Wang.  An Experiment on Efficient Real-Time System Verification through Refutation by Positive Cycles. In Proceedings of the 1st RAMS (Real-time And Media Symposium), Taipei, ROC, July, 1995.
  55. F. Wang.  Reachability Analysis at Procedure Level Through Timing Coincidence.  In Proceedings of the 6th International Conference on Concurrency Theory, Philadelphia, U.S.A., August, 1995. LNCS 962, Springer-Verlag.
  56. F. Wang.  Timing Behavior Analysis for Real-Time Systems. In Proceedings of IEEE Symposium on Logic in Computer Science, San Diego, California, U.S.A., June, 1995.
  57. F. Wang, A.K. Mok.  RTL and Refutation by Positive Cycles. In Proceedings of Formal Methods Europe Symposium, Barcelona, Spain, October, 1994, LNCS 873.
  58. J. Yang, A.K. Mok, F. Wang.  Symbolic Model Checking for Event-Driven Real-Time Systems. In Proceedings of the 1993 IEEE Real-Time System Symposium, IEEE Computer Society. 
  59. F. Wang, A.K. Mok.  A Verifier for Distributed Real-Time Systems with Bounded Integer Variables. In Proceedings of COMPASS Conference, Paithersburg, Maryland, June, 1993.
  60. F. Wang, A.K. Mok, E.A. Emerson.  Symbolic Model-Checking for Distributed Real-Time Systems. In Proceedings of Formal Methods Europe Symposium, Odense, Denmark, April, 1993, LNCS 670.
  61. F. Wang, A.K. Mok.  Asynchronous Real-time Event Logic. In Proceedings of International Computer Symposium, Taichung, Taiwan, December, 1992.
  62. F. Wang, A.K. Mok, E.A. Emerson.  Formal Specification of Asynchronous Distributed Real-Time Systems by APTL. In Proceedings of International Conference on Software Engineering, Melbourne, Australia, May, 1992.