王凡
副研究員

中央研究院
資訊科學研究所
台北市南港區
115
研究院路二段128號

Selected Publications

RESEARCH INTERESTS

Formal Methods
&
Automatic Verification

Farn Wang
Associate Research Fellow

Institute of Information Science
Academia Sinica
Nankang, Taipei
Taiwan 115, ROC

E-mail:
farn@iis.sinica.edu.tw
TEL: +886-2-2788-3799 ext. 1717
FAX: +886-2-2782-4814

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 employed as 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. Since receiving his Ph.D. degree in August 1993, he has worked for the Institute of Information Science, Academia Sinica, Taiwan, R.O.C.

Dr. Farn Wang's is now interested at automating human verification experiences to develop verification tools with high abstractness and efficiency. His current research projects include:

  1. A new BDD-based data-structure, called RED (Region Encoding Diagram), is proposed for the representation of state-spaces of real-time systems. The RED-technology encodes the ordering among fractional parts of dense clock readings into the ordering of variables. Compared with DBM-technology, RED is a canonical minimal form for dense-time state-spaces. Preliminary result is to appear in the proceedings of TACAS'2000, in LNCS, Springer-Verlag, under the title:

    Efficient Data Structure for Fully Symbolic Verification of Real-Time Software Systems

    More details can be found in RED: Region-Encoding Diagrams
  2. In real-world algorithms for concurrent systems, the number of processes In real-world algorithms for concurrent systems, the number of processes in seldom a factor in the correctness of system design. We aim at developing efficient and automatic algorithm to approximately verify such algorithms. A manuscript for the result can be downloaded in the following link. Part of the results
    1. is presented as an invited speech in the first IWTS (International Workshop on Specification and Verification of Timed Systems), Kyoto, Japan, March 3-5, 1999; and
    2. is in the proceedings of FM'99 (Formal Method World Congress), LNCS 1708, Springer-Verlag, under the title

      Automatic Verification of Pointer Data-Structure Systems for All Numbers of Processes

  3. The development of a verification tool called SGM (State-Graph Manipulators) which utilizes a novel packaging approach for verification technique. Traditional verification theory takes several years of graduate study to master. Thus it is very difficult for nonexpert of verification research to benefit from the current research result. In SGM, we use state-graphs as basic data-objects and define manipulators to merge, reduce, and model-check state-graphs. With such a tool, even nonexpert can quickly and efficiently complete their verification tasks. Please check the following link for details.

    SGM: A Real-Time System Verification Tool

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

Dr. Farn Wang is the program co-chair of RTCSA'97 (International Workshop on Real-Time Computing Systems and Applications). He has served in the program committees of IEEE RTAS'96 (Real-Time Technology and Applications Symposium), RTCSA'96, IEEE RTSS'96 (Real-Time System Symposium), IEEE RTAS'97, RTCSA'97, RTCSA'98, RTCSA'99, RTSS'99, ASIAN'99, and RTAS'2000. He was also invited to give a speech at IEEE HASE'98 (High-Assurance Software Engineering). He was also an invited speaker at the 1st IWTS (International Workshop on Specification and Verification of Timed Systems), Kyoto, Japan, March 3-5, 1999.