Email Gateway (Aug 17 2022 at 13:26): Email Gateway (Aug 17 2022 at 13:26):From: Yih-Kuen Tsay <tsay@venus.im.ntu.edu.tw>
[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
Last updated: May 03 2024 at 08:18 UTC