[isabelle] ATVA 2005: Preliminary Program and Call for Participation



[Apologies for multiple copies of this message] 
 
PRELIMINARY PROGRAM AND CALL FOR PARTICIPATION 
 
ATVA 2005 
Third International Symposium on 
Automated Technology for Verification and Analysis 
Taipei, Taiwan, October 4-7, 2005 
http://www.im.ntu.edu.tw/~atva2005/ 
 
HIGHLIGHTS 
. Co-location with FORTE 2005 
. Three Keynote Speeches: 
  . Amir Pnueli  (joint with FORTE 2005) 
  . Zohar Manna 
  . Wolfgang Thomas 
. Three Two-Hour Tutorials, given also by the keynote speakers 
. 33 Contributed Papers 
. Proceedings as LNCS 3707 of Springer 
. Early Registration: by Thursday September 1 
 
Please visit the conference Web site for details. 
 
 
PRELIMINARY PROGRAM 
----- 
Tutorial Day 
Tuesday, October 4, 2005 
(Barry Lam Hall, read "Bo Li Guan" in Chinese, Conference Room 201) 
0830-1000: Registration and Refreshment 
1000-1200: Tutorial I 
  Title: TBA 
  Speaker: Amir Pnueli 
1200-1330: Lunch 
1330-1530: Tutorial II 
  Title: Decision Procedure: Classical Techniques 
  Speaker: Zohar Manna 
1530-1600: Coffee Break 
1600-1800: Tutorial III 
  Title: TBA 
  Speaker: Wolfgang Thomas 
1830-1900: Bus ride to the Reception 
1900-2130: Opening and Reception (joint with FORTE 2005 Banquet) 
 
----- 
Day One of Main Symposium 
Wednesday, October 5, 2005 
(Barry Lam Hall, Auditorium 101) 
0830-0930: Keynote Speech I (joint with FORTE 2005) 
  Title: Ranking Abstraction as a Companion to Predicate Abstraction 
  Speaker: Amir Pnueli 
0930-1000: Coffee Break 
1000-1200: Model Checking 
  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 
  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) 
1830-2030: Committees Meeting 
 
----- 
Day Two of Main Symposium 
Thursday, October 6, 2005 
(Barry Lam Hall, Auditorium 101) 
0830-0930: Keynote Speech II 
  Title: Termination and Invariance Analysis of Loops 
  Speaker: Zohar Manna 
0930-1000: Coffee Break 
1000-1200: Timed, Embedded, and Hybrid Systems (I) 
  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 
1330-1530: Abstraction and Reduction Techniques 
  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) 
  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 
 
1600-1800: Established Formalisms and Standards (Parallel Session) 
  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 
  Title: Some Perspectives of Infinite-State Verification 
  Authors: Wolfgang Thomas 
0930-1000: Coffee Break 
1000-1100: Compositional Verification and Games 
  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) 
  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 
1330-1530: Protocols Analysis, Case Studies, and Tools 
  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 
  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: Closing 
 





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.