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 BibTeX

Keynote Speeches

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

Model Checking

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

Combined Methods

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

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
Electronic Edition (link) BibTeX
A. Dubey, X. Wu, H. Su, T. J. Koo:
Computation Platform for Automatic Analysis of Embedded Software Systems Using Model Based Approach. 114-128
Electronic Edition (link) BibTeX
Andrei Voinikonis:
Quantitative and Qualitative Analysis of Temporal Aspects of Complex Activities. 129-143
Electronic Edition (link) BibTeX
Geng-Dian Huang, Farn Wang:
Automatic Test Case Generation with Region-Related Coverage Annotations for Real-Time Systems. 144-158
Electronic Edition (link) BibTeX

Abstraction and Reduction Techniques

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

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
Electronic Edition (link) BibTeX
Isao Yagi, Yoshiaki Takata, Hiroyuki Seki:
A Static Analysis Using Tree Automata for XML Access Control. 234-247
Electronic Edition (link) BibTeX
Stéphane Demri, David Nowak:
Reasoning About Transfinite Sequences. 248-262
Electronic Edition (link) BibTeX
Bernd Finkbeiner, Sven Schewe:
Semi-automatic Distributed Synthesis. 263-277
Electronic Edition (link) BibTeX

Established Formalisms and Standards

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

Compositional Verification and Games

Purandar Bhaduri:
Synthesis of Interface Automata. 338-353
Electronic Edition (link) BibTeX
Sharon Shoham, Orna Grumberg:
Multi-valued Model Checking Games. 354-369
Electronic Edition (link) BibTeX

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
Electronic Edition (link) BibTeX
Fuzhi Wang, Marta Z. Kwiatkowska:
An MTBDD-Based Implementation of Forward Reachability for Probabilistic Timed Automata. 385-399
Electronic Edition (link) BibTeX

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
Electronic Edition (link) BibTeX
Pierre Combes, David Harel, Hillel Kugler:
Modeling and Verification of a Telecommunication Application Using Live Sequence Charts and the Play-Engine Tool. 414-428
Electronic Edition (link) BibTeX
Moonzoo Kim, Kyo Chul Kang:
Formal Construction and Verification of Home Service Robots: A Case Study. 429-443
Electronic Edition (link) BibTeX
Gary Lindstrom, Peter C. Mehlitz, Willem Visser:
Model Checking Real Time Java Using Java PathFinder. 444-456
Electronic Edition (link) BibTeX

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
Electronic Edition (link) BibTeX
Sébastien Bardin, Alain Finkel, Jérôme Leroux, Ph. Schnoebelen:
Flat Acceleration in Symbolic Model Checking. 474-488
Electronic Edition (link) BibTeX
Jérôme Leroux, Grégoire Sutre:
Flat Counter Automata Almost Everywhere! 489-503
Electronic Edition (link) BibTeX