4. ATVA 2006: Beijing, China

Keynote Speeches

• Mihalis Yannakakis:
  Analysis of Recursive Probabilistic Models. 1-5
  
• Jin Yang:
  Verification Challenges and Opportunities in the New Era of Microprocessor Design. 6-7
  
• Thomas Ball:
  Automated Abstraction of Software. 8
  

Regular Papers

• Alastair F. Donaldson, Alice Miller:
  Symmetry Reduction for Probabilistic Model Checking Using Generic Representatives. 9-23
  
• Parosh Aziz Abdulla, Noomene Ben Henda, Richard Mayr, Sven Sandberg:
  Eager Markov Chains. 24-38
  
• Fei He, Xiaoyu Song, Ming Gu, Jia-Guang Sun:
  A Probabilistic Learning Approach for Counterexample Guided Abstraction Refinement. 39-50
  
• Ming-Ying Chung, Gianfranco Ciardo, Andy Jinqing Yu:
  A Fine-Grained Fullness-Guided Chaining Heuristic for Symbolic Reachability Analysis. 51-66
  
• Pao-Ann Hsiung, Shang-Wei Lin, Yean-Ru Chen, Chun-Hsian Huang, Jia-Jen Yeh, Hong-Yu Sun, Chao-Sheng Lin, Hsiao-Win Liao:
  Model Checking Timed Systems with Urgencies. 67-81
  
• Chao Wang, Zijiang Yang, Franjo Ivancic, Aarti Gupta:
  Whodunit? Causal Analysis for Counterexamples. 82-95
  
• Salvatore La Torre, Margherita Napoli, Mimmo Parente:
  On the Membership Problem for Visibly Pushdown Languages. 96-109
  
• Orna Kupferman, Robby Lampert:
  On the Construction of Fine Automata for Safety Properties. 110-124
  
• Benjamin Aminof, Orna Kupferman:
  On the Succinctness of Nondeterminism. 125-140
  
• Dejvuth Suwimonteerabuth, Stefan Schwoon, Javier Esparza:
  Efficient Algorithms for Alternating Pushdown Systems with an Application to the Computation of Certificate Chains. 141-153
  
• Fei Xie, Guowu Yang, Xiaoyu Song:
  Compositional Reasoning for Hardware/Software Co-verification. 154-169
  
• Wonhong Nam, Rajeev Alur:
  Learning-Based Symbolic Assume-Guarantee Reasoning with Automatic Decomposition. 170-185
  
• Bow-Yaw Wang:
  On the Satisfiability of Modular Arithmetic Formulae. 186-199
  
• Malte Helmert, Robert Mattmüller, Sven Schewe:
  Selective Approaches for Solving Weak Games. 200-214
  
• Thierry Cachat:
  Controller Synthesis and Ordinal Automata. 215-228
  
• Tomohiro Yoneda, Chris J. Myers:
  Effective Contraction of Timed STGs for Decomposition Based Timed Circuit Synthesis. 229-244
  
• Sven Schewe:
  Synthesis for Probabilistic Environments. 245-259
  
• Jinfeng Huang, Marc Geilen, Jeroen Voeten, Henk Corporaal:
  Branching-Time Property Preservation Between Real-Time Systems. 260-275
  
• Werner Damm, Stefan Disch, Hardi Hungar, Jun Pang, Florian Pigorsch, Christoph Scholl, Uwe Waldmann, Boris Wirtz:
  Automatic Verification of Hybrid Systems with Large Discrete State Space. 276-291
  
• Patricia Bouyer, Serge Haddad, Pierre-Alain Reynier:
  Timed Unfoldings for Networks of Timed Automata. 292-306
  
• Franck Cassez, Thomas Chatain, Claude Jard:
  Symbolic Unfoldings for Networks of Timed Automata. 307-321
  
• Harald Fecher, Michael Huth:
  Ranked Predicate Abstraction for Branching Time: Complete, Incremental, and Precise. 322-336
  
• Houda Bel Mokadem, Béatrice Bérard, Patricia Bouyer, François Laroussinie:
  Timed Temporal Logics for Abstracting Transient States. 337-351
  
• Songtao Xia, Ben Di Vito, César Muñoz:
  Predicate Abstraction of Programs with Non-linear Computation. 352-368
  
• Puneet Bhateja, Paul Gastin, Madhavan Mukund:
  A Fresh Look at Testing for Asynchronous Communication. 369-383
  
• M. C. Dharmadeep, K. Gopinath:
  Proactive Leader Election in Asynchronous Shared Memory Systems. 384-398
  
• Laura Brandán Briones, Ed Brinksma, Mariëlle Stoelinga:
  A Semantic Framework for Test Coverage. 399-414
  
• Giorgio Delzanno, Javier Esparza, Jirí Srba:
  Monotonic Set-Extended Prefix Rewriting and Verification of Recursive Ping-Pong Protocols. 415-429
  
• Ye Zhang, Hanne Riis Nielson:
  Analyzing Security Protocols in Hierarchical Networks. 430-445
  
• Colin J. Fidge, Yu-Chu Tian:
  Functional Analysis of a Real-Time Protocol for Networked Control Systems. 446-460
  
• Fernando Rosa Velardo, David de Frutos-Escrig:
  Symbolic Semantics for the Verification of Security Properties of Mobile Petri Nets. 461-476
  
• Ralf Wimmer, Marc Herbstritt, Holger Hermanns, Kelley Strampp, Bernd Becker:
  Sigref- A Symbolic Bisimulation Tool Box. 477-492
  
• Stéphane Demri, Alain Finkel, Valentin Goranko, Govert van Drimmelen:
  Towards a Model-Checker for Counter Systems. 493-507
  
• Peter Niebert, Hongyang Qu:
  The Implementation of Mazurkiewicz Traces in POEM. 508-522
  
• Hang Su, Graham Hemingway, Kai Chen, T. John Koo:
  Model-Based Tool-Chain Infrastructure for Automated Analysis of Embedded Systems. 523-537