This is the list of papers accepted by ATVA2005.

1. Verifying Very Large Industrial Circuits Using 100 Processes and Beyond [SpringerLink]
   Limor Fix, Orna Grumberg, Tamir Heyman, Assaf Schuster
2. A New Reachability Algorithm for Symmetric Multi-processor Architecture [SpringerLink]
   Debashis Sahoo, Jawahar Jain, Subramanian Iyer, David Dill
3. Comprehensive Verification Framework for Dependability of Self-optimizing Systems [SpringerLink]
   Y. Zhao and M. Kardos and S. Oberthuer and F.J. Rammig
4. Exploiting Hub States in Automatic Verification [SpringerLink]
   Giuseppe Della Penna, Igor Melatti, Benedetto Intrigila, Enrico Tronci
5. An Approach for the Verification of SystemC Designs using AsmL [SpringerLink]
   Ali Habibi and Sofiene Tahar
6. Decomposition-Based Verification of Cyclic Workflows [SpringerLink]
   Yongsun Choi and J. Leon Zhao
7. Guaranteed Termination in the Verification of LTL Properties of Non-linear Robust Discrete Time Hybrid Systems [SpringerLink]
   Werner Damm, Guilherme Pinto, Stefan Ratschan
8. Computation Platform for Automatic Analysis of Embedded Software Systems Using Model Based Approach [SpringerLink]
   A. Dubey, X. Wu, H. Su, T. J. Koo
9. Quantitative and Qualitative Analysis of Temporal Aspects of Complex Activities [SpringerLink]
   Andrei Voinikonis
10. Automatic Test Case Generation with Region-Related Coverage Annotations for Real-time Systems [SpringerLink]
    Farn Wang, Geng-Dian Huang, and Rong-Shiung Wu
11. Selective Search in Bounded Model Checking of Reachability Properties [SpringerLink]
    Maciej Szreter
12. Predicate Abstraction of RTL Verilog Descriptions using Constraint Logic Programming [SpringerLink]
    Tun Li, Yang Guo, SiKun Li, Dan Zhu
13. State Space Exploration of Object-Based Systems using Equivalence Reduction and the Sweepline Method [SpringerLink]
    Charles A. Lakos, Lars M. Kristensen
14. Syntactical Colored Petri Nets Reductions [Slides][SpringerLink]
    S. Evangelista, S.Haddad, J.-F. Pradat-Peyre
15. Algorithmic Algebraic Model Checking II: Decidability of Semi-Algebraic Model Checking and its Applications to Systems Biology [SpringerLink]
    V. Mysore, C. Piazza and B. Mishra
16. A Static Analysis using Tree Automata for XML Access Control [SpringerLink]
    Isao YAGI, Yoshiaki TAKATA, and Hiroyuki SEKI
17. Reasoning about transfinite sequences (extended abstract) [Slides] [SpringerLink]
    Stephane Demri and David Nowak
18. Semi-Automatic Distributed Synthesis [SpringerLink]
    Bernd Finkbeiner and Sven Schewe
19. A new graph of classes for the preservation of quantitative temporal constraints [SpringerLink]
    Xiaoyu Mao, Janette Cardoso, Robert Valette
20. Comparison of Different Semantics for Time Petri Nets [Slides][SpringerLink]
    B. Berard, F. Cassez, S. Haddad, D. Lime, O.H. Roux
21. Introducing Dynamic Properties with Past Temporal Operators in the B Refinement [SpringerLink]
    Mouna SAAD and Leila JEMNI BEN AYED
22. Approximate Reachability for Dead Code Elimination in Esterel* [SpringerLink]
    Olivier Tardieu and Stephen A. Edwards
23. Synthesis of Interface Automata [SpringerLink]
    Purandar Bhaduri
24. Multi-Valued Model Checking Games [SpringerLink]
    Sharon Shoham and Orna Grumberg
25. Model Checking Prioritized Timed Automata with Multiple Priorities [SpringerLink]
    Shang-Wei Lin, Pao-Ann Hsiung, Chun-Hsian Hwang, and Yean-Ru Chen
26. MTBDD-based implementation of forward reachability for Probabilistic Timed Automata [SpringerLink]
    Fuzhi Wang and Marta Kwiatkowska
27. An EFSM-based intrusion detection system for ad hoc networks [SpringerLink]
    Jean-Marie Orset, Baptiste Alcalde and Ana Cavalli
28. Modeling and Verification of a Telecommunication Application using Live Sequence Charts and the Play-Engine Tool [Slides][SpringerLink]
    Pierre Combes, David Harel and Hillel Kugler
29. Formal Construction and Verification of Home Service Robots: A Case Study [Slides][SpringerLink]
    Moonzoo Kim, Kyo Chul Kang
30. Model Checking Real Time Java Using Java PathFinder [Slides][SpringerLink]
    Gary Lindstrom, Peter C. Mehlitz, and Willem Visser
31. Using Parametric Automata for the Verification of the Stop-and-Wait Class of Protocols [SpringerLink]
    Guy Edward Gallasch and Jonathan Billington
32. Flat acceleration in symbolic model checking [SpringerLink]
    Sebastien Bardin, Alain Finkel, Jerome Leroux, Philippe Schnoebelen
33. Flat counter automata almost everywhere! [SpringerLink]
    Jerome Leroux and Gregoire Sutre