10. VMCAI 2009: Savannah, GA, USA

Invited Talks

• E. Allen Emerson:
  Model Checking: Progress and Problems. 1
  
• Aarti Gupta:
  Model Checking Concurrent Programs. 2
  
• Mooly Sagiv:
  Thread-Modular Shape Analysis. 3
  

Invited Tutorials

• Byron Cook:
  Advances in Program Termination and Liveness. 4
  
• Véronique Cortier:
  Verification of Security Protocols. 5-13
  

Submitted Papers

• Hasan Amjad, Richard Bornat:
  Towards Automatic Stability Analysis for Rely-Guarantee Proofs. 14-28
  
• William C. Benton, Charles N. Fischer:
  Mostly-Functional Behavior in Java Programs. 29-43
  
• Christos Dimoulas, Mitchell Wand:
  The Higher-Order Aggregate Update Problem. 44-58
  
• Kousha Etessami, Patrice Godefroid:
  An Abort-Aware Model of Transactional Programming. 59-73
  
• Andy Galloway, Gerald Lüttgen, Jan Tobias Mühlberg, Radu Siminiceanu:
  Model-Checking the Linux Virtual File System. 74-88
  
• Patrice Godefroid, Nir Piterman:
  LTL Generalized Model Checking Revisited. 89-104
  
• Kalpana Gondi, Yogeshkumar Patel, A. Prasad Sistla:
  Monitoring the Full Range of omega-Regular Properties of Stochastic Systems. 105-119
  
• Sumit Gulwani, Saurabh Srivastava, Ramarathnam Venkatesan:
  Constraint-Based Invariant Inference over Predicate Abstraction. 120-135
  
• Dilian Gurov, Marieke Huisman:
  Reducing Behavioural to Structural Properties of Programs with Procedures. 136-150
  
• Andreas Holzer, Christian Schallhart, Michael Tautschnig, Helmut Veith:
  Query-Driven Program Testing. 151-166
  
• Marcin Jurdzinski, Ranko Lazic, Michal Rutkowski:
  Average-Price-per-Reward Games on Hybrid Automata with Strong Resets. 167-181
  
• Mark Kattenbelt, Marta Z. Kwiatkowska, Gethin Norman, David Parker:
  Abstraction Refinement for Probabilistic Software. 182-197
  
• Nicholas Kidd, Thomas W. Reps, Julian Dolby, Mandana Vaziri:
  Finding Concurrency-Related Bugs Using Random Isolation. 198-213
  
• Johannes Kinder, Florian Zuleger, Helmut Veith:
  An Abstract Interpretation-Based Framework for Control Flow Reconstruction from Binaries. 214-228
  
• Vincent Laviron, Francesco Logozzo:
  SubPolyhedra: A (More) Scalable Approach to Infer Linear Inequalities. 229-244
  
• Patrick Maier:
  Deciding Extensions of the Theories of Vectors and Bags. 245-259
  
• Matthew Might, Panagiotis Manolios:
  A PosterioriSoundness for Non-deterministic Abstract Interpretations. 260-274
  
• Rotem Oshman:
  An Automata-Theoretic Dynamic Completeness Criterion for Bounded Model-Checking. 275-289
  
• Zvonimir Rakamaric, Alan J. Hu:
  A Scalable Memory Model for Low-Level Code. 290-304
  
• Ankur Taly, Sumit Gulwani, Ashish Tiwari:
  Synthesizing Switching Logic Using Constraint Solving. 305-319
  
• Richard J. Trefler, Thomas Wahl:
  Extending Symmetry Reduction by Exploiting System Architecture. 320-334
  
• Viktor Vafeiadis:
  Shape-Value Abstraction for Verifying Linearizability. 335-348
  
• Ou Wei, Arie Gurfinkel, Marsha Chechik:
  Mixed Transition Systems Revisited. 349-365
  
• Ralf Wimmer, Bettina Braitling, Bernd Becker:
  Counterexample Generation for Discrete-Time Markov Chains Using Bounded Model Checking. 366-380