Automated Technology for Verification and Analysis

1. Front Matter

   PDF

2. Keynote Speeches

   1. Ranking Abstraction as a Companion to Predicate Abstraction

      • Amir Pnueli

      Pages 1-1

   2. Termination and Invariance Analysis of Loops

      • Aaron Bradley, Zohar Manna

      Pages 2-2

   3. Some Perspectives of Infinite-State Verification

      • Wolfgang Thomas

      Pages 3-10

3. Model Checking

   1. Verifying Very Large Industrial Circuits Using 100 Processes and Beyond

      • Limor Fix, Orna Grumberg, Amnon Heyman, Tamir Heyman, Assaf Schuster

      Pages 11-25

   2. A New Reachability Algorithm for Symmetric Multi-processor Architecture

      • Debashis Sahoo, Jawahar Jain, Subramanian Iyer, David Dill

      Pages 26-38

   3. Comprehensive Verification Framework for Dependability of Self-optimizing Systems

      • Y. Zhao, M. Kardos, S. Oberthür, F. J. Rammig

      Pages 39-53

   4. Exploiting Hub States in Automatic Verification

      • Giuseppe Della Penna, Igor Melatti, Benedetto Intrigila, Enrico Tronci

      Pages 54-68

4. Combined Methods

   1. An Approach for the Verification of SystemC Designs Using AsmL

      • Ali Habibi, Sofiène Tahar

      Pages 69-83

   2. Decomposition-Based Verification of Cyclic Workflows

      • Yongsun Choi, J. Leon Zhao

      Pages 84-98

5. Timed, Embedded, and Hybrid Systems (I)

   1. Guaranteed Termination in the Verification of LTL Properties of Non-linear Robust Discrete Time Hybrid Systems

      • Werner Damm, Guilherme Pinto, Stefan Ratschan

      Pages 99-113

   2. Computation Platform for Automatic Analysis of Embedded Software Systems Using Model Based Approach

      • A. Dubey, X. Wu, H. Su, T. J. Koo

      Pages 114-128

   3. Quantitative and Qualitative Analysis of Temporal Aspects of Complex Activities

      • Andrei Voinikonis

      Pages 129-143

   4. Automatic Test Case Generation with Region-Related Coverage Annotations for Real-Time Systems

      • Geng-Dian Huang, Farn Wang

      Pages 144-158

6. Abstraction and Reduction Techniques

   1. Selective Search in Bounded Model Checking of Reachability Properties

      • Maciej Szreter

      Pages 159-173

   2. Predicate Abstraction of RTL Verilog Descriptions Using Constraint Logic Programming

      • Tun Li, Yang Guo, SiKun Li, GongJie Liu

      Pages 174-186

   3. State Space Exploration of Object-Based Systems Using Equivalence Reduction and the Sweepline Method

      • Charles A. Lakos, Lars M. Kristensen

      Pages 187-201

   4. Syntactical Colored Petri Nets Reductions

      • S. Evangelista, S. Haddad, J. -F. Pradat-Peyre

      Pages 202-216

7. Decidability and Complexity

   1. Algorithmic Algebraic Model Checking II: Decidability of Semi-algebraic Model Checking and Its Applications to Systems Biology

      • V. Mysore, C. Piazza, B. Mishra

      Pages 217-233

   2. A Static Analysis Using Tree Automata for XML Access Control

      • Isao Yagi, Yoshiaki Takata, Hiroyuki Seki

      Pages 234-247

The Automated Technology for Veri?cation and Analysis (ATVA) international symposium series was initiated in 2003, responding to a growing interest in formal veri?cation spurred by the booming IT industry, particularly hardware design and manufacturing in East Asia. Its purpose is to promote research on automated veri?cation and analysis in the region by providing a forum for int- action between the regional and the international research/industrial commu- ties of the ?eld. ATVA 2005, the third of the ATVA series, was held in Taipei, Taiwan, October 4–7, 2005. The main theme of the symposium encompasses - sign, complexities, tools, and applications of automated methods for veri?cation and analysis. The symposium was co-located and had a two-day overlap with FORTE 2005, which was held October 2–5, 2005. We received a total of 95 submissions from 17 countries. Each submission was assigned to three Program Committee members, who were helped by their subreviewers, for rigorous and fair evaluation. The ?nal deliberation by the P- gram Committee was conducted over email for a duration of about 10 days after nearly all review reports had been collected. In the end, 33 papers were - lectedforinclusionintheprogram.ATVA2005hadthreekeynotespeechesgiven respectively by Amir Pnueli (joint with FORTE 2005), Zohar Manna, and Wo- gang Thomas. The main symposium was preceded by a tutorial day, consisting of three two-hour lectures given also by the keynote speakers.

• Hub
• Java
• XML
• automata
• complexity
• formal methods
• hybrid systems
• logic
• model checking
• petri net
• program analysis
• programming
• protocol verification
• refinement
• systems design

• Department of Computer Science, Bar Ilan University, Ramat Gan, Israel

  Doron A. Peled

• Department of Information Management, National Taiwan University, Taiwan

  Yih-Kuen Tsay

Policies and ethics