Computer Aided Verification

1. Front Matter

   PDF

2. Invited Tutorials

   1. Transactional Memory: Glimmer of a Theory

      • Rachid Guerraoui, Michał Kapałka

      Pages 1-15

   2. Mixed-Signal System Verification: A High-Speed Link Example

      • Jaeha Kim

      Pages 16-16

   3. Modelling Epigenetic Information Maintenance: A Kappa Tutorial

      • Jean Krivine, Vincent Danos, Arndt Benecke

      Pages 17-32

   4. Component-Based Construction of Real-Time Systems in BIP

      • Joseph Sifakis

      Pages 33-34

3. Invited Talks

   1. Models and Proofs of Protocol Security: A Progress Report

      • Martín Abadi, Bruno Blanchet, Hubert Comon-Lundh

      Pages 35-49

   2. Predictability vs. Efficiency in the Multicore Era: Fight of Titans or Happy Ever after?

      • Luca Benini

      Pages 50-50

   3. SPEED: Symbolic Complexity Bound Analysis

      • Sumit Gulwani

      Pages 51-62

   4. Regression Verification: Proving the Equivalence of Similar Programs

      • Ofer Strichman

      Pages 63-63

4. Regular Papers

   1. Symbolic Counter Abstraction for Concurrent Software

      • Gérard Basler, Michele Mazzucchi, Thomas Wahl, Daniel Kroening

      Pages 64-78

   2. Priority Scheduling of Distributed Systems Based on Model Checking

      • Ananda Basu, Saddek Bensalem, Doron Peled, Joseph Sifakis

      Pages 79-93

   3. Explaining Counterexamples Using Causality

      • Ilan Beer, Shoham Ben-David, Hana Chockler, Avigail Orni, Richard Trefler

      Pages 94-108

   4. Size-Change Termination, Monotonicity Constraints and Ranking Functions

      • Amir M. Ben-Amram

      Pages 109-123

   5. Linear Functional Fixed-points

      • Nikolaj Bjørner, Joe Hendrix

      Pages 124-139

   6. Better Quality in Synthesis through Quantitative Objectives

      • Roderick Bloem, Krishnendu Chatterjee, Thomas A. Henzinger, Barbara Jobstmann

      Pages 140-156

   7. Automatic Verification of Integer Array Programs

      • Marius Bozga, Peter Habermehl, Radu Iosif, Filip Konečný, Tomáš Vojnar

      Pages 157-172

   8. Automated Analysis of Java Methods for Confidentiality

      • Pavol Černý, Rajeev Alur

      Pages 173-187

   9. Requirements Validation for Hybrid Systems

      • Alessandro Cimatti, Marco Roveri, Stefano Tonetta

      Pages 188-203

   10. Towards Performance Prediction of Compositional Models in Industrial GALS Designs

       • Nicolas Coste, Holger Hermanns, Etienne Lantreibecq, Wendelin Serwe

       Pages 204-218

   11. Image Computation for Polynomial Dynamical Systems Using the Bernstein Expansion

       • Thao Dang, David Salinas

       Pages 219-232

This book constitutes the refereed proceedings of the 21st International Conference on Computer Aided Verification, CAV 2009, held in Grenoble, France, in June/July 2009. The 36 revised full papers presented together with 16 tool papers and 4 invited talks and 4 invited tutorials were carefully reviewed and selected from 135 regular paper and 34 tool paper submissions. The papers are dedicated to the advancement of the theory and practice of computer-aided formal analysis methods for hardware and software systems; their scope ranges from theoretical results to concrete applications, with an emphasis on practical verification tools and the underlying algorithms and techniques.

• algorithms
• assertion
• automata theory
• automatic verification
• computational logic
• computer
• concurrency
• constraint solving
• debugging
• decision making
• declarative networking
• dynamic verification
• formal methods
• formal ve
• verification

• LIAFA, University Paris Diderot (Paris 7), Case 7014, Paris Cedex 13, France

  Ahmed Bouajjani

• Verimag, Centre Equation, Gières, France

  Oded Maler

Policies and ethics