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]
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
Last updated: May 03 2024 at 08:18 UTC