[isabelle] ATVA 2005: Call for Participation

[Apologies for multiple copies of this message] 
ATVA 2005 
Third International Symposium on 
Automated Technology for Verification and Analysis 
Taipei, Taiwan, October 4-7, 2005 
. Co-located with FORTE 2005 
. Three Keynote Speeches: 
  . Amir Pnueli  (joint with FORTE) 
  . Zohar Manna 
  . Wolfgang Thomas 
. Three Two-Hour Tutorials, by the keynote speakers 
. 33 Technical Papers 
. Proceedings as LNCS 3707 of Springer 
. Early Registration: by Thursday September 1 
Below is the preliminary program.
Please visit the conference Web site for further details. 
ATVA 2005 
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: Decision Procedure: Classical Techniques 
  Speaker: Zohar Manna 
1200-1330: Lunch 
1330-1530: Tutorial II 
  Title: Automata Theoretic Foundations of Infinite Games 
  Speaker: Wolfgang Thomas 
1530-1600: Coffee Break 
1600-1800: Tutorial III 
  Title: Program Synthesis in Action  
  Speaker: Amir Pnueli 
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.