Forsyth Park Fountain; image taken from German Wikipedia
Tenth International Conference on
Verification, Model Checking, and Abstract Interpretation
January 18-20, 2009
Savannah, GA, USA (co-located with POPL 2009)
Program
Sunday, January 18, 2009
9:00-10:10 Welcome and Invited Talk (Chair: Neil Jones)-
Model Checking: Progress and Problems
E. Allen Emerson (University of Texas at Austin)
Coffee break
10:30-12:00 Abstract Interpretation (Chair: Patrick Cousot)
-
A Posteriori Soundness for Non-deterministic Abstract Interpretations
Matthew Might and Panagiotis Manolios -
SubPolyhedra: A (More) Scalable Approach to Infer Linear
Inequalities
Vincent Laviron and Francesco Logozzo -
An Abstract Interpretation-Based Framework for Control Flow Reconstruction from Binaries
Johannes Kinder, Helmut Veith, and Florian Zuleger
Lunch break
13:30-15:00 Invited Tutorial (Chair: Markus Müller-Olm)
- Verification of Security Protocols
(slides)
Véronique Cortier (LORIA, CNRS, Nancy)
Coffee break
15:30-17:30 Concurrency (Chair: Dave Schmidt)
-
An Abort-Aware Model of Transactional Programming
Kousha Etessami and Patrice Godefroid -
Shape-value Abstraction for Verifying Linearizability
Viktor Vafeiadis -
Towards Automatic Stability Analysis for Rely-Guarantee Proofs
Hasan Amjad and Richard Bornat -
Finding Concurrency-Related Bugs using Random Isolation
Nicholas Kidd, Thomas Reps, Julian Dolby, and Mandana Vaziri
Monday, January 19, 2009
9:00-10:00 Invited Talk (Chair: Lenore Zuck)- Model Checking Concurrent Programs
(slides)
Aarti Gupta (NEC Labs America)
Coffee break
10:30-12:00 Stochastic Methods (Chair: Véronique Cortier)
-
Abstraction Refinement for Probabilistic Software
Mark Kattenbelt, Marta Kwiatkowska, Gethin Norman, and David Parker -
Counterexample
Generation for Discrete-time Markov Chains using Bounded
Model Checking
Ralf Wimmer, Bettina Braitling, and Bernd Becker -
Monitoring the Full Range of Omega-regular Properties of Stochastic Systems
Kalpana Gondi, Yogeshkumar Patel, and A. Prasad Sistla
Lunch break
13:30-15:00 Invited Tutorial (Chair: Mooly Sagiv)
-
Proving Program Termination and Liveness
(slides)
Byron Cook (Microsoft Research, Cambridge)
Coffee break
15:30-17:30 Model Checking (Chair: Andrey Rybalchenko)
-
An Automata-Theoretic Dynamic Completeness Criterion for Bounded Model-Checking
Rotem Oshman -
Extending Symmetry Reduction by Exploiting System Architecture
Thomas Wahl and Richard Trefler -
Mixed Transition Systems Revisited
Ou Wei, Arie Gurfinkel, and Marsha Chechik -
LTL Generalized Model Checking Revisited
Patrice Godefroid and Nir Piterman
Conference Dinner (7 PM Sapphire Grill at 110 West Congress Street)
Tuesday, January 20, 2009
9:00-10:00 Invited Talk (Chair: Neil Jones)-
Thread Modular Shape Analysis
Mooly Sagiv (Tel-Aviv University) (slides)
Coffee break
10:30-12:00 Program Analysis (Chair: Francesco Logozzo)
-
The Higher-order Aggregate Update Problem
Christos Dimoulas and Mitchell Wand -
Constraint-based Invariant Inference over Predicate Abstraction
Sumit Gulwani, Saurabh Srivastava, and Ramarathnam Venkatesan -
Mostly-functional Behavior in Java Programs
William Benton and Charles Fischer
Lunch break
13:30-15:00 Theory (Chair: Markus Müller-Olm)
-
Average-Price/Reward Games on Hybrid Automata with Strong Resets
Michal Rutkowski, Marcin Jurdzinski, and Ranko Lazic -
Deciding Extensions of the Theories of Vectors and Bags
Patrick Maier -
Reducing Behavioural to Structural Properties of Programs with Procedures
Dilian Gurov and Marieke Huisman
Coffee break
15:30-17:30 Testing, Synthesis, and Verification (Chair: Aarti Gupta)
-
Query-Driven Program Testing
Andreas Holzer, Christian Schallhart, Michael Tautschnig, and Helmut Veith -
Synthesizing Switching Logic using Constraint Solving
Ankur Taly, Sumit Gulwani, and Ashish Tiwari -
Model-Checking the Linux Virtual File System
Radu Siminiceanu, Andy Galloway, Gerald Lüttgen, and Tobias Mühlberg -
A Scalable Memory Model for Low-Level Code
Zvonimir Rakamaric and Alan Hu