9. VMCAI 2008: San Francisco, CA, USA

• Radhia Cousot:
  Abstract Interpretation of Non-monotone Bi-inductive Semantic Definitions. 1-3
  
• Neil D. Jones, René Rydhof Hansen:
  CTL as an Intermediate Language. 4
  
• Orna Kupferman, Yoad Lustig:
  Multi-valued Logics, Automata, Simulations, and Games. 5
  
• Jens Palsberg:
  Verification of Register Allocators. 6
  
• Marco Pistoia:
  Program Analysis and Programming Languages for Security. 7
  
• Roberto Bagnara, Patricia M. Hill, Enea Zaffanella:
  An Improved Tight Closure Algorithm for Integer Octagonal Constraints. 8-21
  
• Parosh Aziz Abdulla, Noomene Ben Henda, Giorgio Delzanno, Ahmed Rezine:
  Handling Parameterized Systems with Non-atomic Global Conditions. 22-36
  
• Olivier Bouissou, Matthieu Martel:
  Abstract Interpretation of the Physical Inputs of Embedded Programs. 37-51
  
• Alessandro Cimatti, Marco Roveri, Viktor Schuppan, Andrei Tchaltsev:
  Diagnostic Information for Realizability. 52-67
  
• Vijay D'Silva, Mitra Purandare, Daniel Kroening:
  Approximation Refinement for Interpolation-Based Model Checking. 68-82
  
• Vincent Danos, Jérôme Feret, Walter Fontana, Jean Krivine:
  Abstract Interpretation of Cellular Signalling Networks. 83-97
  
• Rayna Dimitrova, Andreas Podelski:
  Is Lazy Abstraction a Decision Procedure for Broadcast Protocols? 98-111
  
• Harald Fecher, Michael Huth:
  Model Checking for Action Abstraction. 112-126
  
• Eugene Goldberg:
  On Bridging Simulation and Formal Verification. 127-141
  
• Alex Groce, Rajeev Joshi:
  Extending Model Checking with Dynamic Analysis. 142-156
  
• Isabella Mastroeni:
  Deriving Bisimulations by Simplifying Partitions. 157-171
  
• Mario Méndez-Lojo, Manuel V. Hermenegildo:
  Precise Set Sharing Analysis for Java-Style Programs. 172-187
  
• Yannick Moy:
  Sufficient Preconditions for Modular Assertion Checking. 188-202
  
• Huu Hai Nguyen, Viktor Kuncak, Wei-Ngan Chin:
  Runtime Checking for Separation Logic. 203-217
  
• Ruzica Piskac, Viktor Kuncak:
  Decision Procedures for Multisets with Cardinality Constraints. 218-232
  
• Amir Pnueli, Yaniv Sa'ar:
  All You Need Is Compassion. 233-247
  
• Francesco Ranzato, Olivia Rossi-Doria, Francesco Tapparo:
  A Forward-Backward Abstraction Refinement Algorithm. 248-262
  
• David A. Schmidt:
  Internal and External Logics of Abstract Interpretations. 263-278
  
• Andreas Morgenstern, Klaus Schneider:
  From LTL to Symbolically Represented Deterministic Automata. 279-293
  
• A. Prasad Sistla, Abhigna R. Srinivas:
  Monitoring Temporal Properties of Stochastic Systems. 294-308
  
• Saqib Sohail, Fabio Somenzi, Kavita Ravi:
  A Hybrid Algorithm for LTL Games. 309-323