7. ATVA 2009: Macao, China

Invited Talks

• Mark R. Greenstreet:
  Verifying VLSI Circuits. 1-20
  
• Orna Grumberg:
  3-Valued Abstraction for (Bounded) Model Checking. 21
  
• A. W. Roscoe, P. J. Armstrong, Pragyesh:
  Local Search in Model Checking. 22-38
  

State Space Reduction

• Jaco Geldenhuys, Henri Hansen, Antti Valmari:
  Exploring the Scope for Partial Order Reduction. 39-53
  
• Jaco van de Pol, Mark Timmer:
  State Space Reduction of Linear Processes Using Control Flow Reconstruction. 54-68
  
• Mika Cohen, Mads Dam, Alessio Lomuscio, Hongyang Qu:
  A Data Symmetry Reduction Technique for Temporal-epistemic Logic. 69-83
  

Tools

• Joakim Byg, Kenneth Yrke Jørgensen, Jirí Srba:
  TAPAAL: Editor, Simulator and Verifier of Timed-Arc Petri Nets. 84-89
  
• Stephen Fenech, Gordon J. Pace, Gerardo Schneider:
  CLAN: A Tool for Contract Analysis and Conflict Discovery. 90-96
  
• Michal Kebrt, Ondrej Sery:
  UnitCheck: Unit Testing and Model Checking Combined. 97-103
  

Probabilistic Systems

• Taolue Chen, Tingting Han, Joost-Pieter Katoen, Alexandru Mereacre:
  LTL Model Checking of Time-Inhomogeneous Markov Chains. 104-119
  
• Diana El Rabih, Nihal Pekergin:
  Statistical Model Checking Using Perfect Simulation. 120-134
  
• Christel Baier, Marcus Größer, Frank Ciesinski:
  Quantitative Analysis under Fairness Constraints. 135-150
  
• Jens Oehlerking, Oliver E. Theel:
  A Decompositional Proof Scheme for Automated Convergence Proofs of Stochastic Hybrid Systems. 151-165
  

Medley

• Guanhua He, Shengchao Qin, Chenguang Luo, Wei-Ngan Chin:
  Memory Usage Verification Using Hip/Sleek. 166-181
  
• Oliver Friedmann, Martin Lange:
  Solving Parity Games in Practice. 182-196
  
• Parosh Aziz Abdulla, Muhsin Atto, Jonathan Cederberg, Ran Ji:
  Automated Analysis of Data-Dependent Programs with Dynamic Memory. 197-212
  

Temporal Logic I

• Alexandre Duret-Lutz, Denis Poitrenaud, Jean-Michel Couvreur:
  On-the-fly Emptiness Check of Transition-Based Streett Automata. 213-227
  
• Hrishikesh Karmarkar, Supratik Chakraborty:
  On Minimal Odd Rankings for Büchi Complementation. 228-243
  
• Christian Dax, Felix Klaedtke, Stefan Leue:
  Specification Languages for Stutter-Invariant Regular Properties. 244-254
  

Abstraction and Refinement

• Ansgar Fehnker, Ralf Huuck, Sean Seefried:
  Incremental False Path Elimination for Static Software Analysis. 255-270
  
• Yael Meller, Orna Grumberg, Sharon Shoham:
  A Framework for Compositional Verification of Multi-valued Systems via Abstraction-Refinement. 271-288
  
• Alarico Campetelli, Alexander Gruler, Martin Leucker, Daniel Thoma:
  Don't Know for Multi-valued Systems. 289-305
  
• Jacob M. Howe, Andy King:
  Logahedra: A New Weakly Relational Domain. 306-320
  

Fault Tolerant Systems

• Rayna Dimitrova, Bernd Finkbeiner:
  Synthesis of Fault-Tolerant Distributed Systems. 321-336
  
• Sandip Ray, Kecheng Hao, Yan Chen, Fei Xie, Jin Yang:
  Formal Verification for High-Assurance Behavioral Synthesis. 337-351
  
• Franck Cassez, Jérémy Dubreil, Hervé Marchand:
  Dynamic Observers for the Synthesis of Opaque Systems. 352-367
  

Temporal Logic II

• Yang Zhao, Gianfranco Ciardo:
  Symbolic CTL Model Checking of Asynchronous Systems Using Constrained Saturation. 368-381
  
• Geng-Dian Huang, Lin-Zan Cai, Farn Wang:
  LTL Model Checking for Recursive Programs. 382-396
  
• Hongtao Huang:
  On Detecting Regular Predicates in Distributed Systems. 397-411