Tutorial Day
Tuesday, October 4, 2005
(Barry Lam Hall, or "Bo Li Guan" in Chinese, Conference Room 201)
0830-1000 Registration
1000-1200 Tutorial I (Chair: Jieh Hsiang)
Title: Decision Procedures for Verification
Speaker: Zohar Manna
1200-1330 Lunch
1330-1530 Tutorial II (Chair: Hsu-Chun Yen)
Title: Automata Theoretic Foundations of Infinite Games
Speaker: Wolfgang Thomas
1530-1600 Coffee Break
1600-1800 Tutorial III (Chair: Doron A. Peled)
Title: Program Synthesis in Action
Speaker: Amir Pnueli
1830-1900 Bus ride to the Reception
1900-2130 Reception (joint with FORTE 2005 Banquet)

 

Day One of Main Symposium
Wednesday, October 5, 2005
(Barry Lam Hall, Auditorium 101)
0830-0835 Opening (Chairs: Doron A. Peled and Yih-Kuen Tsay)
0835-0935 Keynote Speech I, joint with FORTE (Chair: Farn Wang)
Title: Ranking Abstraction as a Companion to Predicate Abstraction
Speaker: Amir Pnueli
0935-1000 Coffee Break
1000-1200 Model Checking (Chair: Pao-Ann Hsiung)
Verifying Very Large Industrial Circuits Using 100 Processes and Beyond
Authors: Limor Fix, Orna Grumberg, Amnon Heyman, Tamir Heyman, and Assaf Schuster

A New Reachability Algorithm for Symmetric Multi-processor Architecture
Authors: Debashis Sahoo, Jawahar Jain, Subramanian Iyer, and David Dill

Comprehensive Verification Framework for Dependability of Self-optimizing Systems
Authors: Y. Zhao and M. Kardos and S. Oberthuer and F.J. Rammig

Exploiting Hub States in Automatic Verification
Authors: Giuseppe Della Penna, Igor Melatti, Benedetto Intrigila, and Enrico Tronci
1200-1230 Coffee Break (quick lunch now or after the next short session)
1230-1330 Combined Methods (Chair: Teruo Higashino)
An Approach for the Verification of SystemC Designs using AsmL
Authors: Ali Habibi and Sofiene Tahar

Decomposition-Based Verification of Cyclic Workflows
Authors: Yongsun Choi and J. Leon Zhao
1400-1800 Excursion (joint with FORTE 2005)

 

Day Two of Main Symposium
Thursday, October 6, 2005
(Barry Lam Hall, Auditorium 101)
0830-0930 Keynote Speech II (Chair: Amir Pnueli)
Title: Termination and Invariance Analysis of Loops
Speaker: Zohar Manna
0930-1000 Coffee Break
1000-1200 Timed, Embedded, and Hybrid Systems (I) (Chair: Yih-Kuen Tsay)
Guaranteed Termination in the Verification of LTL Properties of Non-linear Robust Discrete Time Hybrid Systems
Authors: Werner Damm, Guilherme Pinto, and Stefan Ratschan

Computation Platform for Automatic Analysis of Embedded Software Systems Using Model Based Approach
Authors: A. Dubey, X. Wu, H. Su, and T.J. Koo

Quantitative and Qualitative Analysis of Temporal Aspects of Complex Activities
Authors: Andrei Voinikonis

Automatic Test Case Generation with Region-Related Coverage Annotations for Real-time Systems
Authors: Geng-Dian Huang and Farn Wang
1200-1330 Lunch and Business Meeting (open to all participants)
1330-1530 Abstraction and Reduction Techniques (Chair: Chung-Yang Huang)
Selective Search in Bounded Model Checking of Reachability Properties
Authors: Maciej Szreter

Predicate Abstraction of RTL Verilog Descriptions using Constraint Logic Programming
Authors: Tun Li, Yang Guo, SiKun Li, and GongJie Liu

State Space Exploration of Object-Based Systems using Equivalence Reduction and the Sweepline Method
Authors: Charles A. Lakos and Lars M. Kristensen

Title: Syntactical Colored Petri Nets Reductions
Authors: S. Evangelista, S.Haddad, J.-F. Pradat-Peyre
1530-1600 Coffee Break
1600-1800

Decidability and Complexity: Parallel Session A (Chair: Bow-Yaw Wang)
Algorithmic Algebraic Model Checking II: Decidability of Semi-Algebraic Model Checking and its Applications to Systems Biology
Authors: V. Mysore, C. Piazza, and B. Mishra

A Static Analysis using Tree Automata for XML Access Control
Authors: Isao Yagi, Yoshiaki Takata, and Hiroyuki Seki

Reasoning about Transfinite Sequences
Authors: Stephane Demri and David Nowak

Semi-Automatic Distributed Synthesis
Authors: Bernd Finkbeiner and Sven Schewe

Established Formalisms and Standards: Parallel Session B (Chair: Yung-Pin Cheng)
A New Graph of Classes for the Preservation of Quantitative Temporal Constraints
Authors: Xiaoyu Mao, Janette Cardoso, and Robert Valette

Comparison of Different Semantics for Time Petri Nets
Authors: B. Berard, F. Cassez, S. Haddad, Didier Lime, and O.H. Roux

Introducing Dynamic Properties with Past Temporal Operators in the B Refinement
Authors: Mouna Saad and Leila Jemni Ben Ayed

Approximate Reachability for Dead Code Elimination in Esterel*
Authors: Olivier Tardieu and Stephen A. Edwards
1830-1900 Bus ride to the Banquet
1900-2130

Banquet

 

Day Three of Main Symposium
Friday, October 7, 2005
(Barry Lam Hall, Auditorium 101)
0830-0930 Keynote Speech III (Chair: Doron A. Peled)
Title: Some Perspectives of Infinite-State Verification
Authors: Wolfgang Thomas
0930-1000 Coffee Break
1000-1100

Compositional Verification and Games (Chair: Wolfgang Thomas)
Synthesis of Interface Automata
Authors: Purandar Bhaduri

Multi-Valued Model Checking Games
Authors: Sharon Shoham and Orna Grumberg

1100-1200 Timed, Embedded, and Hybrid Systems (II) (Chair: Wolfgang Thomas)
Model Checking Prioritized Timed Automata
Authors: Shang-Wei Lin, Pao-Ann Hsiung, Chun-Hsian Huang, and Yean-Ru Chen

An MTBDD-based Implementation of Forward Reachability for Probabilistic Timed Automata
Authors: Fuzhi Wang and Marta Kwiatkowska
1200-1330 Lunch / Committees Meeting
1330-1530 Protocols Analysis, Case Studies, and Tools (Chair: Sofiene Tahar)
An EFSM-based Intrusion Detection System for Ad Hoc Networks
Authors: Jean-Marie Orset, Baptiste Alcalde, and Ana Cavalli

Modeling and Verification of a Telecommunication Application using Live Sequence Charts and the Play-Engine Tool
Authors: Pierre Combes, David Harel, and Hillel Kugler

Formal Construction and Verification of Home Service Robots: A Case Study
Authors: Moonzoo Kim and Kyo Chul Kang

Model Checking Real Time Java Using Java PathFinder
Authors: Gary Lindstrom, Peter C. Mehlitz, and Willem Visser
1530-1600

Coffee Break
1600-1730 Infinite-State and Parameterized Systems (Chair: Yih-Kuen Tsay)
Using Parametric Automata for the Verification of the Stop-and-Wait Class of Protocols
Authors: Guy Edward Gallasch and Jonathan Billington

Flat Acceleration in Symbolic Model Checking
Authors: Sebastien Bardin, Alain Finkel, Jerome Leroux, and Philippe Schnoebelen

Flat Counter Automata Almost Everywhere!
Authors: Jerome Leroux and Gregoire Sutre
1730-1800

Presentation of the Best Paper Award
Closing