ATVA'2003 Program                                                        

Wednesday 10 December 2003

8:30-9:00        Registration

9:00-9:15        Tutorial Opening

9:15-11:15      Tutorial I: Model Checking Systems with Multiple Similar Processes

                            Professor E. Allen Emerson, Univ. of Texas, Austin, USA

                            Session Chair: Farn Wang

11:15-13:00    Lunch

13:00-15:00    Tutorial II: Verification of Real-Time Systems with BDD-like Data-Structures

                            Professor Farn Wang, National Taiwan University, Taiwan, ROC

                            Session Chair: Hsu-Chun Yen

                            Abstract, Power Point file for presentation

15:00-15:30    break

15:30-17:30    Tutorial III: Algorithmic Testing

                            Professor Doron A. Peled, University of Warwick, UK

                            Session Chair: Yih-Kuen Tsay

                            Abstract, PowerPoint file

18:00-20:00    Reception

Thursday 11 December 2003

8:30-9:00        Registration

9:00-9:15        Workshop Opening

9:15-10:15      Keynote Speech I: The State of Formal Verification: Model Checking and Beyond

                           Professor E. Allen Emerson, Univ. of Texas, Austin, USA

                      Session Chair: Hsu-Chun Yen

10:15-10:30    break

10:30-12:00    Session A: Software Verification, Session Chair: Yih-Kuen Tsay

                            A.1 Creating a Formal Verification Platform for IBM CoreConnect-based SoC

                                Wen-Shiu Liao, Pao-Ann Hsiung

                            A.2 Using SPIN to Model Cryptographic Protocols

                                Li Yongjian, Xue Rui

                            A3 Analyzing Interoperability of Protocols Using Model Checking

                                Peng Wu

12:00-14:00    lunch

14:00-16:00    Session B: SOC and Protocol Verification, Session chair: Bow-Yaw Wang

                            B.1, Invited Speech:  Enforcing Concurrent Temporal Behavior

                                Professor Doron A. Peled

                                Abstract

                            B.2, Reasoning about Systems with Many Data Values

                            without Data Independence Assumption

                                Yung-Pin Cheng, Keh-Ren Wu

                            B.3, SCENATOR: a Prototype Tool for Requirements Inconsistency Detection

                                Ridha, Khedri, Rong Wu, Bahati Sanga

                            B.4, Defining the Semantics of UML Class and Sequence Diagrams

                                for Ensuring the Consistency and Executability

                                of OO Software Specification

                                Franck Xia, Gautam S. Kane

16:00-16:30    break

16:30-18:00    Session C: Foundamental Frameworks (I), Session Chair: Yung-Pin Cheng

                            C.1 Behavioral Unfolding of Formal Specifications

                            Based on Communicating automata

                                Nicolas RAPIN

                            C.2 Regular Expressions for Run-Time Verification

                                Usa Sammapun, Oleg Sokolsky

                            C.3 Towards a Temporal Logic tLTL for the Verification

                            of Rewriting Theories denoting ECATNets

                                Hacene Sebih, Kamel Barkaoui, Mohamed Bettaz, Faiza Belala, Zaidi Sahnoun

Friday 12 December 2003

9:00-10:00        Keynote Speech II: Counter Machines and Verification of Infinite-State Systems

                            Professor Oscar H. Ibarra, Univ. of California, Santa Barbara, USA

                                           Hsu-Chun Yen, National Taiwan University, Taiwan, ROC

                            Session Chair: Yih-Kuen Tsay

                            Abstract

10:00-10:30      break

10:30-18:00      lunch & tour

18:00-20:00      Banquet

Saturday 13 December 2003

9:00-10:00        Keynote Speech III:

                            Prof. Doron A. Peled, University of Warwick, UK

                            Session Chair: Farn Wang

                            Abstract, PowerPoint file

10:00-10:30      break

10:30-12:00      Session E: Foundamental frameworks (II), Session Chair: Pao-Ann Hsiung

                            D.1 Practical Model Checking of LTL with Past

                                M. Pradella, P. San Pietro, P. Spoletini, A. Morzenti

                            D.2 A Framework for Modeling and Analysis

                            of Real-time System Operating System.

                                Jin Hyun Kim, Jin Young Choi  

                            D.3 Verification and Realization for the Distributed Parallel Systems based on An

                                Extended Petri Net and XML/Java Executor" for ATVA2003.

                                Shin'nosuke Yamaguchi  

12:00-13:00      Business meeting

13:00-13:30      Closing.