[Apologies for multiple copies of this message] 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-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 _________________________________________________________________________________ mozart-users mailing list [email protected] http://www.mozart-oz.org/mailman/listinfo/mozart-users
