Selected Publications

I. Journal articles

  1. F. Wang, G.-D. Huang, F. Yu.  TCTL Inevitability Analysis of Dense-Time Systems: From Theory to Engineering.  To appear in IEEE Transactions on Software Engineering, IEEE Computer Society. 
  2. 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
  3. 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. 
  4. 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. 
  5. 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. 
  6. 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. 
  7. F. WangEfficient 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.
  8. 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. 
  9. F. Wang, P.-A. Hsiung.  Efficient and User-Friendly Verification.  IEEE Transactions on Computers 51(1), Jan. 2002, ISSN 0018-9340, pp.61-84. 
  10. F. Wang Parametric Analysis of Computer Systems. Journal of Formal Methods in Systems Design 17, 2000, pp.39-60, Kluwer Academic Publishers.
  11. 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.
  12. 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)
  13. 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.
  14. 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.
  15. 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. F. Wang.  Efficient Model-Checking of Dense-Time Systems with Time-Convexity Analysis.  RTSS 2008, Dec. 2008, Barcelona.  IEEE Computer Society. 
  2. F. Wang.  Time-Progress Evaluation for Dense-Time Automata with Concave Path Conditions.  ATVA 2008, Oct. 2008, Seoul.  LNCS, Springer-Verlag. 
  3. 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]
  4. F. Wang, Chih-Hong Cheng.  Program Repair Suggestions from Graphical State-Transition Specifications.   FORTE 2008, June 2008, Tokyo.  LNCS 5048, Springer-Verlag. [PPT file]
  5. 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]
  6. F. WangSymbolic 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]
  7. G.-D. Huang, F. WangAutomatic 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.   
  8. 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. 
  9. 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. 
  10. F. Wang.   Symbolic Parametric Safety Analysis of Linear Hybrid Systems with BDD-like Data-StructuresCAV 2004, LNCS 3114, Springer-Verlag; Boston, USA, July 2004. 
  11. F. WangModel-Checking Distributed Real-Time Systems with States, Events, and Multiple Fairness Assumptions.   AMAST 2004, LNCS 3116, Springer-Verlga; Stirling, UK, July 2004. 
  12. 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.
  13. 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. 
  14. 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. 
  15. F. Wang, G.-D. Huang, F. Yu.  Symbolic Simulation of Real-Time Concurrent Systems. RTCSA’2003, LNCS 2968, Springer-Verlag.  
  16. 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. 
  17. 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.
  18. F. WangSymmetric Model-Checking of Concurrent Timed Automata with Clock-Restriction Diagram, RTCSA’2002, March 18-20, 2002, Tokyo, Japan.
  19. F. WangRED: 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.  
  20. 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.  
  21. 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. 
  22. F. WangRegion Encoding Diagram for Fully Symbolic Verification of Real-Time Systems.  24'th COMPSAC'2000 (Computer Software and Applications Conference), Oct, 2000.
  23. F. WangEfficient Data Structure for Fully Symbolic Verification of Real-Time Software Systems.  TACAS'2000, LNCS 1785, Springer-Verlag.
  24. P.-A. Hsiung, Y.-S. Kuo, F. Wang Verification of Concurrent Client-Server Real-Time Scheduling Systems.  RTCSA'99, Dec., 1999, IEEE press.
  25. P.-A. Hsiung, F. WangUser-Friendly Verification.  FORTE/PSTV'99 (FORmal description TEchnique/Protocol Specification, Testing, Verification), October, 1999. 
  26. F. WangAutomatic Verification of Pointer Data-Structure Systems for All Numbers of Processes.  FM'99 (Formal Method World Congress), September 1999, LNCS 1708, Springer-Verlag.
  27. 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.
  28. P.-A. Hsiung, F. WangA State Graph Manipulator Tool for Real-Time System Specification and Verification. 1998 RTCSA (Real-Time Computing Systems and Applications) Workshop, October 1998, Hiroshima, Japan.
  29. 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.
  30. 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)
  31. 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
  32. 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.
  33. 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.
  34. 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
  35. 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.
  36. 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.
  37. 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.
  38. F. WangReachability 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.
  39. F. WangTiming Behavior Analysis for Real-Time Systems. In Proceedings of IEEE Symposium on Logic in Computer Science, San Diego, California, U.S.A., June, 1995.
  40. F. Wang, A.K. Mok.  RTL and Refutation by Positive Cycles. In Proceedings of Formal Methods Europe Symposium, Barcelona, Spain, October, 1994, LNCS 873.
  41. J. Yang, A.K. Mok, F. WangSymbolic Model Checking for Event-Driven Real-Time Systems. In Proceedings of the 1993 IEEE Real-Time System Symposium, IEEE Computer Society. 
  42. 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.
  43. 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.
  44. F. Wang, A.K. Mok.  Asynchronous Real-time Event Logic. In Proceedings of International Computer Symposium, Taichung, Taiwan, December, 1992.
  45. 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.