Automated Technology for Verification and Analysis

1. Front Matter

   PDF

2. Invited Papers

   1. Statistical Model Checking for Cyber-Physical Systems

      • Edmund M. Clarke, Paolo Zuliani

      Pages 1-12

   2. Max and Sum Semantics for Alternating Weighted Automata

      • Shaull Almagor, Orna Kupferman

      Pages 13-27

   3. Making Software Verification Tools Really Work

      • Jade Alglave, Alastair F. Donaldson, Daniel Kroening, Michael Tautschnig

      Pages 28-42

   4. Synthesizing, Verifying, and Debugging SoC with FSM-Based Specification of On-Chip Communication Protocols

      • Masahiro Fujita

      Pages 43-50

   5. Automated Analysis of Industrial Embedded Software

      • Moonzoo Kim, Yunho Kim

      Pages 51-59

3. Regular Papers

   1. Nondeterministic Update of CTL Models by Preserving Satisfaction through Protections

      • Miguel Carrillo, David A. Rosenblueth

      Pages 60-74

   2. Type-Based Automated Verification of Authenticity in Asymmetric Cryptographic Protocols

      • Morten Dahl, Naoki Kobayashi, Yunde Sun, Hans Hüttel

      Pages 75-89

   3. Formalization of Finite-State Discrete-Time Markov Chains in HOL

      • Liya Liu, Osman Hasan, Sofiène Tahar

      Pages 90-104

   4. An Alternative Definition for Timed Automata Composition

      • Jean-Paul Bodeveix, Abdeldjalil Boudjadar, Mamoun Filali

      Pages 105-119

   5. Model Checking EGF on Basic Parallel Processes

      • Hongfei Fu

      Pages 120-134

   6. Measuring Permissiveness in Parity Games: Mean-Payoff Parity Games Revisited

      • Patricia Bouyer, Nicolas Markey, Jörg Olschewski, Michael Ummels

      Pages 135-149

   7. Algorithms for Synthesizing Priorities in Component-Based Systems

      • Chih-Hong Cheng, Saddek Bensalem, Yu-Fang Chen, Rongjie Yan, Barbara Jobstmann, Harald Ruess et al.

      Pages 150-167

   8. Trust Metrics for the SPKI/SDSI Authorisation Framework

      • Dominik Wojtczak

      Pages 168-182

   9. Antichain-Based QBF Solving

      • Thomas Brihaye, Véronique Bruyère, Laurent Doyen, Marc Ducobu, Jean-Francois Raskin

      Pages 183-197

   10. A Hierarchical Approach for the Synthesis of Stabilizing Controllers for Hybrid Systems

       • Janusz Malinowski, Peter Niebert, Pierre-Alain Reynier

       Pages 198-212

   11. Formal Analysis of Online Algorithms

       • Benjamin Aminof, Orna Kupferman, Robby Lampert

       Pages 213-227

   12. Modal Transition Systems: Composition and LTL Model Checking

       • Nikola Beneš, Ivana Černá, Jan Křetínský

       Pages 228-242

   13. Efficient Inclusion Checking on Explicit and Semi-symbolic Tree Automata

       • Lukáš Holík, Ondřej Lengál, Jiří Šimáček, Tomáš Vojnar

       Pages 243-258

   14. Assembling Sessions

       • Philippe Darondeau, Loïc Hélouët, Madhavan Mukund

       Pages 259-274

This book constitutes the refereed proceedings of the 9th International Symposium on Automated Technology for Verification and Analysis, ATVA 2011, held in Taipei, Taiwan, in October 2011.
The 23 revised regular papers presented together with 5 invited papers, 11 short papers, and 2 tool papers, were carefully reviewed and selected from 75 submissions. The papers address all theoretical and practical aspects of automated analysis, verification and synthesis; thus providing a forum for interaction between the regional and the international research communities and industry in the field.

• basic parallel processes
• fault tolerant modeling
• hybrid systems
• model checking
• timed automata

• University of California, Santa Barbara, USA

  Tevfik Bultan

• Department of Computer Science and Information Engineering, National Chung Cheng University, Chiayi, Taiwan, ROC

  Pao-Ann Hsiung

Policies and ethics