Verification, Model Checking, and Abstract Interpretation

1. Front Matter

   PDF

2. Invited Talks

   1. Analysis of Systems with Stochastic Process Creation

      • Javier Esparza

      Pages 1-1

   2. Verifying Concurrent Programs with Chalice

      • K. Rustan M. Leino

      Pages 2-2

   3. Static Timing Analysis for Hard Real-Time Systems

      • Reinhard Wilhelm, Sebastian Altmeyer, Claire Burguière, Daniel Grund, Jörg Herter, Jan Reineke et al.

      Pages 3-22

3. Invited Tutorials

   1. Abstract Interpretation-Based Protection

      • Roberto Giacobazzi

      Pages 23-24

   2. Advances in Probabilistic Model Checking

      • Joost-Pieter Katoen

      Pages 25-25

   3. Building a Calculus of Data Structures

      • Viktor Kuncak, Ruzica Piskac, Philippe Suter, Thomas Wies

      Pages 26-44

4. Regular Papers

   1. Temporal Reasoning for Procedural Programs

      • Rajeev Alur, Swarat Chaudhuri

      Pages 45-60

   2. Improved Model Checking of Hierarchical Systems

      • Benjamin Aminof, Orna Kupferman, Aniello Murano

      Pages 61-77

   3. Path-Oriented Reachability Verification of a Class of Nonlinear Hybrid Automata Using Convex Programming

      • Lei Bu, Jianhua Zhao, Xuandong Li

      Pages 78-94

   4. Complexity Bounds for the Verification of Real-Time Software

      • Rohit Chadha, Axel Legay, Pavithra Prabhakar, Mahesh Viswanathan

      Pages 95-111

   5. An Abstract Domain to Discover Interval Linear Equalities

      • Liqian Chen, Antoine Miné, Ji Wang, Patrick Cousot

      Pages 112-128

   6. Interpolant Strength

      • Vijay D’Silva, Daniel Kroening, Mitra Purandare, Georg Weissenbacher

      Pages 129-145

   7. Checking Bounded Reachability in Asynchronous Systems by Symbolic Event Tracing

      • Jori Dubrovin

      Pages 146-162

   8. Invariant and Type Inference for Matrices

      • Thomas A. Henzinger, Thibaud Hottelier, Laura Kovács, Andrei Voronkov

      Pages 163-179

   9. Deriving Invariants by Algorithmic Learning, Decision Procedures, and Predicate Abstraction

      • Yungbum Jung, Soonho Kong, Bow-Yaw Wang, Kwangkeun Yi

      Pages 180-196

   10. Automatic Abstraction for Congruences

       • Andy King, Harald Søndergaard

       Pages 197-213

   11. Shape Analysis of Low-Level C with Overlapping Structures

       • Jörg Kreiker, Helmut Seidl, Vesal Vojdani

       Pages 214-230

   12. Abstract Threads

       • Shuvendu K. Lahiri, Alexander Malkis, Shaz Qadeer

       Pages 231-246

   13. Shape Analysis with Reference Set Relations

       • Mark Marron, Rupak Majumdar, Darko Stefanovic, Deepak Kapur

       Pages 247-262

This volume contains the proceedings of the 11th International Conference on Veri?cation, Model Checking, and Abstract Interpretation (VMCAI 2010), held in Madrid, Spain, January 17–19, 2010. VMCAI 2010 was the 11th in a series of meetings. Previous meetings were held in Port Je?erson (1997), Pisa (1998), Venice (2002), New York (2003), Venice(2004),Paris(2005),Charleston(2006),Nice(2007),SanFrancisco(2008), and Savannah (2009). 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 21 papers out of 57 submissions based on anonymous reviews and discussions in an electronic Program Committee me- ing. The principal selection criteria were relevance and quality.

• Debugging
• abstract interpretation
• debugging techniques
• deductive methods
• formal methods
• formal verif
• model checking
• optimization
• program analysis
• program certification
• program semantics
• program verification
• static analysis
• type systems
• verification
• algorithm analysis and problem complexity

• Facultad de Informatica (UPM), IMDEA Software, Madrid, Spain

  Gilles Barthe

• Facultad de Informatica (UPM), IMDEA Software and Technical University of Madrid, Madrid, Spain

  Manuel Hermenegildo

Policies and ethics