VMCAI'07 Preliminary Schedule

January 14th

9:00 - 10:00: Invited Speaker

• DIVINE: DIscovering Variables IN eXecutables,
  Thomas Reps

10:00 - 10:30: Coffee Break

10:30 - 12:30: Paper Session

• Verifying Compensating Transactions,
  Michael Emmi and Rupak Majumdar
• Model Checking Nonblocking MPI Programs,
  Stephen F. Siegel
• Model Checking via Gamma-CFA,
  Matthew Might, Benjamin Chambers and Olin Shivers
• Using First-Order Theorem Provers in the Jahob Data Structure Verification System,
  Charles Bouillaguet, Viktor Kuncak, Thomas Wies, Karen Zee and Martin Rinard

12:30 - 14:30: Lunch Break

14:30 - 15:30: Invited Tutorial

• Interpolants and Symbolic Model Checking,
  Ken McMillan

15:30 - 16:00: Coffee Break

16:00 - 17:30: Paper Session

• Shape Analysis of Single-Parent Heaps,
  Ittai Balaban, Amir Pnueli and Lenore Zuck
• An Inference-Rule-Based Decision Procedure for Verification of Heap-Manipulating Programs with Mutable Data and Cyclic Data Structures,
  Zvonimir Rakamaric, Jesse Bingham and Alan Hu
• On Flat Programs with Lists,
  Radu Iosif and Marius Bozga

19:00 - Late: Banquet

• Details to follow

January 15th

9:00 - 10:00: Invited Speaker

• Automata-Theoretic Model Checking Revisited,
  Moshe Y. Vardi

10:00 - 10:30: Coffee Break

10:30 - 12:30: Paper Session

• Language-Based Abstraction Refinement for Hybrid System Verification,
  Felix Klaedtke, Stefan Ratschan and Zhikun She
• More precise partition abstractions,
  Harald Fecher and Michael Huth
• The Spotlight Principle - On Combining Process-Summarizing State Abstractions,
  Bjoern Wachter and Bernd Westphal
• Lattice Automata,
  Yoad Lustig and Orna Kupferman

12:30 - 14:30: Lunch Break

14:30 - 15:30: Invited Tutorial

• Learning Algorithms and Formal Verification,
  Madhusudan Parthasarathy

15:30 - 16:00: Coffee Break

16:00 - 17:30: Paper Session

• Constructing Specialized Shape Analyses for Uniform Change,
  Tal Lev-Ami, Mooly Sagiv, Neil Immerman and Thomas Reps
• Maintaining Structural Invariants in Shape Analysis with Local Reasoning,
  Sigmund Cherem and Radu Rugina
• Automated Verification of Shape and Size Properties via Separation Logic,
  Huu Hai Nguyen, Cristina David, Shengchao Qin and Wei-Ngan Chin

January 16th

9:00 - 10:00: Invited Speaker

• Towards Shape Analysis for Device Drivers,
  Hongseok Yang

10:00 - 10:30: Coffee Break

10:30 - 12:30: Paper Session

• An Abstract Domain Extending Difference-Bound Matrices with Disequality Constraints,
  Mathias Peron and Nicolas Halbwachs
• Cibai: An abstract interpretation-based static analyzer for modular analysis and verification of Java classes,
  Francesco Logozzo
• Symmetry and Completeness in the Analysis of Parameterized Systems,
  Kedar Namjoshi
• Better Under-approximation of Programs by Hiding Variables,
  Thomas Ball and Orna Kupferman

12:30 - 14:30: Lunch Break

14:30 - 15:30: Invited Tutorial

• The Constraint Database Approach to Software Verification,
  Peter Revesz

16:00 - 17:30: Paper Session

• Constraint Solving for Interpolation,
  Andrey Rybalchenko and Viorica Sofronie-Stokkermans.
• Assertion Checking Unified,
  Sumit Gulwani and Ashish Tiwari.
• Invariant Synthesis for Combined Theories,
  Dirk Beyer, Thomas Henzinger, Rupak Majumdar and Andrey Rybalchenko