Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Farn Wang
[go: Go Back, main page]

王凡
副教授

國立台灣大學
電機工程學系

暨研究所
台北市 106

羅斯福路四段一號
　

Selected Publications

Courses

1. Formal Modelling and Verification

2. Operating Systems

3. Discrete Math

　

Pictures

Formal Methods & Automated Verification

　

Farn Wang
Associate Professor

Dept. of Electrical Engineering
National Taiwan University
Nr.1, Sec. 4, Roosevelt Rd.
Taipei, Taiwan 106, ROC

E-mail: farn@cc.ee.ntu.edu.tw
TEL: +886-2-23635251 ext. 435
FAX: +886-2-23671909

Dr. Farn Wang received the degree of Bachelor of Science in Electrical Engineering from National Taiwan University in June 1982.  He received the degree of Master of Science from Natinal Chiao-Tung University in June 1984.  From September 1986 to May 1987, he was a research assistant in Telecommunication Laboratories, Ministry of Communications, R.O.C.  He joined the Ph.D. Program in Mathematics and Computer Science at Dartmouth College in September 1987 and then transfered to the Ph.D. Program in Computer Sciences at the University of Texas at Austin in September 1988.  From August 1993 to October 1997, he was an assistant research fellow in the Institute of Information Science (IIS), Academia Sinica, Taiwan, R.O.C.  From October 1997 to July 2002, he was an associate research fellow at IIS.  In August 2002, he becomes an associate professor at the Department of Electrical Engineering, National Taiwan University.

Dr. Farn Wang's has been working on automated verification technology since 1989.  He has initiated and developed several verification tools with high abstractness and efficiency. His current research projects include:

Recent papers:
  1. Formal Verification of Timed Systems: A Survey and Perspective,   to appear in Proceedings of the IEEE. 
  2. Symbolic Parametric Safety Analysis of Linear Hybrid Systems with BDD-like Data-Structures,  to appear in proceedings of CAV 2004, LNCS, Springer-Verlag; Boston, USA, July 2004. 
  3. Model-Checking Distributed Real-Time Systems with States, Events, and Multiple Fairness Assumptions,  to appear in proceedings of AMAST 2004, LNCS, Springer-Verlga; Stirling, UK, July 2004. 
  4. Numerical coverage estimation for dense-time systems, in proceedings of FORTE'2003, LNCS 2767, Springer-Verlag. 
  5. Speed-up techniques for TCTL greatest fixpoint evaluation, in proceedings of CIAA'2003, LNCS 2759, Springer-Verlag. 
  6. Timing Parameter Characterization of Real-Time Systems, in proceedings of CIAA'2003, LNCS 2759, Springer-Verlag. 
  7. Efficient Verification of Timed Automata with BDD-like Data-Structures,  to appear in the special issue of STTT (Software Tools for Technology Transfer), Springer-Verlag for VMCAI'2003; a preliminary version also in proceedings of 4th VMCAI, Jan 2003, New York City,  in LNCS  2575,  Springer-Verlag.

Tools:

  1. red 5.0: an integrated symbolic TCTL model-checker/simulator for

with GUI, counter-example generation capability, and deadlock-detection capability. 

Reports available on CRD performance comparison (STTT, Springer-Verlag), gfp speed-up (CIAA'03, LNCS 2759, Springer-Verlag), numerical coverage (FORTE'2003, LNCS 2767, Springer-Verlag), HRD. 

  1. red 4.2: a symbolic TCTL model-checker/simulator for timed automata with GUI, counter-example generation capability, and deadlock-detection capability.

  1. SGM: State-Graph Manipulators,  A User-friendly Compositional Verification Tool for real-time systems  

To the date of the last update of this page, SGM has been downloaded by more than 100 users all over the world.

Academic Activities:

program co-chairs:

RTCSA'97 (International Workshop on Real-Time Computing Systems and Applications),

ATVA'2003 (International Workshop on Automated Technology of Verification and Analysis)

ATVA'2004 (International Symposium on Automated Technology of Verification and Analysis)

Special-issue guest editor:

International Jounral of Foundations on Computer Science, special-issue on Verification and Analysis of Infinite-state Systems, Vol. 14, Nr.4, August 2003, World Scientific Publishing Co. 

Tutorials:

1. Verification of Real-Time Systems with BDD-like Data-Structures,

      ATVA 2003, Taipei, Taiwan, ROC, December 2003

2. Symbolic Techniques for the verification of real-time and

    embedded systems with BDD-like datastructures

     FORTE 2004, Madrid, Spain, September 2004

Invited Speeches: :

1. IEEE HASE'98 (High-Assurance Software Engineering).

2. 1st IWTS (International Workshop on Specification and Verification of Timed Systems), Kyoto, Japan, March 3-5,

3. AVIS'2003, Warsaw, Poland

Program Committees:

APSEC'2000, 2001, 2003

ASIAN'99

ATVA'2003

AVIS'2003,

ECRTS'2003, 2004

FORTE'2004

ICFEM'2002, 2003, 2004

IEEE RTAS'96, 97, 2000, 2001, 2004

IEEE RTSS'96, 99, 2000, 2001, 2004

RTCSA'96, 97, 98, 99, 2000, 2002, 2003