Verification, Model Checking, and Abstract Interpretation

1. Front Matter

   PDF

2. Invited Talks

   1. Model Checking: Progress and Problems

      • E. Allen Emerson

      Pages 1-1

   2. Model Checking Concurrent Programs

      • Aarti Gupta

      Pages 2-2

   3. Thread-Modular Shape Analysis

      • Mooly Sagiv

      Pages 3-3

3. Invited Tutorials

   1. Advances in Program Termination and Liveness

      • Byron Cook

      Pages 4-4

   2. Verification of Security Protocols

      • Véronique Cortier

      Pages 5-13

4. Submitted Papers

   1. Towards Automatic Stability Analysis for Rely-Guarantee Proofs

      • Hasan Amjad, Richard Bornat

      Pages 14-28

   2. Mostly-Functional Behavior in Java Programs

      • William C. Benton, Charles N. Fischer

      Pages 29-43

   3. The Higher-Order Aggregate Update Problem

      • Christos Dimoulas, Mitchell Wand

      Pages 44-58

   4. An Abort-Aware Model of Transactional Programming

      • Kousha Etessami, Patrice Godefroid

      Pages 59-73

   5. Model-Checking the Linux Virtual File System

      • Andy Galloway, Gerald Lüttgen, Jan Tobias Mühlberg, Radu I. Siminiceanu

      Pages 74-88

   6. LTL Generalized Model Checking Revisited

      • Patrice Godefroid, Nir Piterman

      Pages 89-104

   7. Monitoring the Full Range of ω-Regular Properties of Stochastic Systems

      • Kalpana Gondi, Yogeshkumar Patel, A. Prasad Sistla

      Pages 105-119

   8. Constraint-Based Invariant Inference over Predicate Abstraction

      • Sumit Gulwani, Saurabh Srivastava, Ramarathnam Venkatesan

      Pages 120-135

   9. Reducing Behavioural to Structural Properties of Programs with Procedures

      • Dilian Gurov, Marieke Huisman

      Pages 136-150

   10. Query-Driven Program Testing

       • Andreas Holzer, Christian Schallhart, Michael Tautschnig, Helmut Veith

       Pages 151-166

   11. Average-Price-per-Reward Games on Hybrid Automata with Strong Resets

       • Marcin Jurdziński, Ranko Lazić, Michał Rutkowski

       Pages 167-181

   12. Abstraction Refinement for Probabilistic Software

       • Mark Kattenbelt, Marta Kwiatkowska, Gethin Norman, David Parker

       Pages 182-197

   13. Finding Concurrency-Related Bugs Using Random Isolation

       • Nicholas Kidd, Thomas Reps, Julian Dolby, Mandana Vaziri

       Pages 198-213

   14. An Abstract Interpretation-Based Framework for Control Flow Reconstruction from Binaries

       • Johannes Kinder, Florian Zuleger, Helmut Veith

       Pages 214-228

This volume contains the proceedings of the 10th International Conference on Veri?cation, Model Checking, and Abstract Interpretation (VMCAI 2009), held in Savannah, Georgia, USA, January 18–20, 2009. VMCAI 2009 was the 10th in a series of meetings. Previous meetings were heldinPortJe?erson1997,Pisa1998,Venice2002,NewYork2003,Venice2004, Paris 2005, Charleston 2006, Nice 2007, and San Francisco 2008. VMCAI centers on state-of-the-art research relevant to analysis of programs and systems and drawn from three research communities: veri?cation, model checking, and abstract interpretation. A goal is to facilitate interaction, cro- fertilization, and the advance of hybrid methods that combine two or all three areas. Topics covered by VMCAI include program veri?cation, program cert- cation, model checking, debugging techniques, abstract interpretation, abstract domains, static analysis, type systems, deductive methods, and optimization. The Program Committee selected 24 papers out of 72 submissions based on anonymous reviews and discussions in an electronic Program Committee me- ing. The principal selection criteria were relevance and quality. VMCAI has a tradition of inviting distinguished speakers to give talks and tutorials. This time the program included three invited talks by: – E. Allen Emerson (University of Texas at Austin) on “Model Checking: Progress and Problems” – Aarti Gupta (NEC Labs, Princeton) on “Model Checking Concurrent Programs” – Mooly Sagiv (Tel-Aviv University) on “Thread Modular Shape Analysis” There were also two invited tutorials by: – Byron Cook (Microsoft Research, Cambridge) on “Proving Program Ter- nation and Liveness” – V´ eroniqueCortier (LORIA, CNRS, Nancy) on“Veri?cationof Security P- tocols”.

• Action
• abstract domains
• abstraction
• debugging techniques
• formal methods
• higher-order languages
• optimization
• program analysis
• program invariants
• program semantics
• program veri
• programming
• programming language
• structured analysis
• verification

• (Emeritus University of Copenhagen), Rungsted, Denmark

  Neil D. Jones

• Institut für Informatik, Fachbereich Mathematik und Informatik, Westfälische Wilhelms-Universität, Münster, Germany

  Markus Müller-Olm

Policies and ethics