3. ATVA 2005: Taipei, Taiwan

Doron Peled, Yih-Kuen Tsay (Eds.): Automated Technology for Verification and Analysis, Third International Symposium, ATVA 2005, Taipei, Taiwan, October 4-7, 2005, Proceedings. Lecture Notes in Computer Science 3707 Springer 2005, ISBN 3-540-29209-8

Keynote Speeches

Amir Pnueli:
Ranking Abstraction as a Companion to Predicate Abstraction, . 1
Aaron R. Bradley, Zohar Manna:
Termination and Invariance Analysis of Loops. 2
Wolfgang Thomas:
Some Perspectives of Infinite-State Verification. 3-10

Model Checking

Limor Fix, Orna Grumberg, Amnon Heyman, Tamir Heyman, Assaf Schuster:
Verifying Very Large Industrial Circuits Using 100 Processes and Beyond. 11-25
Debashis Sahoo, Jawahar Jain, Subramanian K. Iyer, David L. Dill:
A New Reachability Algorithm for Symmetric Multi-processor Architecture. 26-38
Yuhong Zhao, Martin Kardos, Simon Oberthür, Franz J. Rammig:
Comprehensive Verification Framework for Dependability of Self-optimizing Systems. 39-53
Giuseppe Della Penna, Igor Melatti, Benedetto Intrigila, Enrico Tronci:
Exploiting Hub States in Automatic Verification. 54-68

Combined Methods

Ali Habibi, Sofiène Tahar:
An Approach for the Verification of SystemC Designs Using AsmL. 69-83
Yongsun Choi, J. Leon Zhao:
Decomposition-Based Verification of Cyclic Workflows. 84-98

Timed, Embedded, and Hybrid Systems (I)

Werner Damm, Guilherme Pinto, Stefan Ratschan:
Guaranteed Termination in the Verification of LTL Properties of Non-linear Robust Discrete Time Hybrid Systems. 99-113
A. Dubey, X. Wu, H. Su, T. J. Koo:
Computation Platform for Automatic Analysis of Embedded Software Systems Using Model Based Approach. 114-128
Andrei Voinikonis:
Quantitative and Qualitative Analysis of Temporal Aspects of Complex Activities. 129-143
Geng-Dian Huang, Farn Wang:
Automatic Test Case Generation with Region-Related Coverage Annotations for Real-Time Systems. 144-158

Abstraction and Reduction Techniques

Maciej Szreter:
Selective Search in Bounded Model Checking of Reachability Properties. 159-173
Tun Li, Yang Guo, Sikun Li, GongJie Liu:
Predicate Abstraction of RTL Verilog Descriptions Using Constraint Logic Programming. 174-186
Charles A. Lakos, Lars Michael Kristensen:
State Space Exploration of Object-Based Systems Using Equivalence Reduction and the Sweepline Method. 187-201
Sami Evangelista, Serge Haddad, Jean-François Pradat-Peyre:
Syntactical Colored Petri Nets Reductions. 202-216

Decidability and Complexity

Venkatesh Mysore, Carla Piazza, Bud Mishra:
Algorithmic Algebraic Model Checking II: Decidability of Semi-algebraic Model Checking and Its Applications to Systems Biology. 217-233
Isao Yagi, Yoshiaki Takata, Hiroyuki Seki:
A Static Analysis Using Tree Automata for XML Access Control. 234-247
Stéphane Demri, David Nowak:
Reasoning About Transfinite Sequences. 248-262
Bernd Finkbeiner, Sven Schewe:
Semi-automatic Distributed Synthesis. 263-277

Established Formalisms and Standards

Xiaoyu Mao, Janette Cardoso, Robert Valette:
A New Graph of Classes for the Preservation of Quantitative Temporal Constraints. 278-292
Béatrice Bérard, Franck Cassez, Serge Haddad, Didier Lime, Olivier H. Roux:
Comparison of Different Semantics for Time Petri Nets. 293-307
Mouna Saad, Leila Jemni Ben Ayed:
Introducing Dynamic Properties with Past Temporal Operators in the B Refinement. 308-322
Olivier Tardieu, Stephen A. Edwards:
Approximate Reachability for Dead Code Elimination in Esterel. 323-337

Compositional Verification and Games

Purandar Bhaduri:
Synthesis of Interface Automata. 338-353
Sharon Shoham, Orna Grumberg:
Multi-valued Model Checking Games. 354-369

Timed, Embedded, and Hybrid Systems (II)

Shang-Wei Lin, Pao-Ann Hsiung, Chun-Hsian Huang, Yean-Ru Chen:
Model Checking Prioritized Timed Automata. 370-384
Fuzhi Wang, Marta Z. Kwiatkowska:
An MTBDD-Based Implementation of Forward Reachability for Probabilistic Timed Automata. 385-399

Protocols Analysis, Case Studies, and Tools

Jean-Marie Orset, Baptiste Alcalde, Ana R. Cavalli:
An EFSM-Based Intrusion Detection System for Ad Hoc Networks. 400-413
Pierre Combes, David Harel, Hillel Kugler:
Modeling and Verification of a Telecommunication Application Using Live Sequence Charts and the Play-Engine Tool. 414-428
Moonzoo Kim, Kyo Chul Kang:
Formal Construction and Verification of Home Service Robots: A Case Study. 429-443
Gary Lindstrom, Peter C. Mehlitz, Willem Visser:
Model Checking Real Time Java Using Java PathFinder. 444-456

Infinite-State and Parameterized Systems

Guy Edward Gallasch, Jonathan Billington:
Using Parametric Automata for the Verification of the Stop-and-Wait Class of Protocols. 457-473
Sébastien Bardin, Alain Finkel, Jérôme Leroux, Ph. Schnoebelen:
Flat Acceleration in Symbolic Model Checking. 474-488
Jérôme Leroux, Grégoire Sutre:
Flat Counter Automata Almost Everywhere! 489-503