Computer Aided Verification

19th International Conference, CAV 2007, Berlin, Germany, July 3-7, 2007. Proceedings

  • Editors
  • Werner Damm
  • Holger Hermanns
Conference proceedings CAV 2007

Part of the Lecture Notes in Computer Science book series (LNCS, volume 4590)

Table of contents

  1. Front Matter
  2. Invited Talks

  3. Invited Tutorials

    1. Dirk Beyer, Thomas A. Henzinger, Vasu Singh
      Pages 4-19
    2. Leonardo de Moura, Bruno Dutertre, Natarajan Shankar
      Pages 20-36
    3. Gary T. Leavens, Joseph R. Kiniry, Erik Poll
      Pages 37-37
    4. Martin Fränzle
      Pages 38-38
  4. Session I: Compositionality

    1. Nishant Sinha, Edmund Clarke
      Pages 39-54
    2. Ariel Cohen, Kedar S. Namjoshi
      Pages 55-67
  5. Session II: Verification Process

    1. Denis Gopan, Thomas Reps
      Pages 68-81
    2. Sagar Chaki, Christian Schallhart, Helmut Veith
      Pages 82-94
  6. Session III: Timed Synthesis and Games

    1. Oded Maler, Dejan Nickovic, Amir Pnueli
      Pages 95-107
    2. Gerd Behrmann, Agnès Cougnard, Alexandre David, Emmanuel Fleury, Kim G. Larsen, Didier Lime
      Pages 121-125
  7. Session IV: Infinitive State Verification

    1. Bengt Jonsson, Mayank Saksena
      Pages 131-144
    2. Parosh Aziz Abdulla, Giorgio Delzanno, Ahmed Rezine
      Pages 145-157
  8. Session V: Tool Environment

    1. Hubert Garavel, Radu Mateescu, Frédéric Lang, Wendelin Serwe
      Pages 158-163
    2. Dejvuth Suwimonteerabuth, Felix Berger, Stefan Schwoon, Javier Esparza
      Pages 164-167
    3. Nathaniel Charlton, Michael Huth
      Pages 168-172
    4. Jean-Christophe Filliâtre, Claude Marché
      Pages 173-177
  9. Session VI: Shapes

    1. Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter W. O’Hearn, Thomas Wies et al.
      Pages 178-192
    2. Ranjit Jhala, Kenneth L. McMillan
      Pages 193-206
    3. Ahmed Bouajjani, Séverine Fratani, Shaz Qadeer
      Pages 207-220
    4. Igor Bogudlov, Tal Lev-Ami, Thomas Reps, Mooly Sagiv
      Pages 221-225
  10. Session VII: Concurrent Program Verification

    1. Vineet Kahlon, Yu Yang, Sriram Sankaranarayanan, Aarti Gupta
      Pages 226-239
    2. Feng Chen, Grigore Roşu
      Pages 240-253
    3. Gaël Patin, Mihaela Sighireanu, Tayssir Touili
      Pages 254-257
  11. Session VIII: Reactive Designs

    1. Barbara Jobstmann, Stefan Galler, Martin Weiglhofer, Roderick Bloem
      Pages 258-262
    2. Roderick Bloem, Roberto Cavada, Ingo Pill, Marco Roveri, Andrei Tchaltsev
      Pages 263-267
  12. Session IX: Parallelisation

    1. Jonathan Ezekiel, Gerald Lüttgen, Gianfranco Ciardo
      Pages 268-280
    2. Jiri Barnat, Lubos Brim, Pavel Šimeček
      Pages 281-293
  13. Session X: Constraints and Decisions

    1. Robert Brummayer, Armin Biere
      Pages 294-297
    2. Clark Barrett, Cesare Tinelli
      Pages 298-302
    3. Panagiotis Manolios, Sudarshan K. Srinivasan, Daron Vroon
      Pages 303-306
    4. Bernd Becker, Christian Dax, Jochen Eisinger, Felix Klaedtke
      Pages 307-310
  14. Session XI: Probabilistic Verification

    1. Joost-Pieter Katoen, Daniel Klink, Martin Leucker, Verena Wolf
      Pages 311-324
    2. Luca de Alfaro, Pritam Roy
      Pages 325-338
  15. Session XII: Abstraction

    1. Chao Wang, Zijiang Yang, Aarti Gupta, Franjo Ivančić
      Pages 352-365
    2. Domagoj Babić, Alan J. Hu
      Pages 366-378
    3. Thomas Wahl
      Pages 393-405
  16. Session XIII: Assume-Guarantee Reasoning

    1. Orna Kupferman, Nir Piterman, Moshe Y. Vardi
      Pages 406-419
    2. Anubhav Gupta, Kenneth L. McMillan, Zhaohui Fu
      Pages 420-432
  17. Session XIV: Hybrid Systems

  18. Session XV: Program Analysis

    1. Daphna Amit, Noam Rinetzky, Thomas Reps, Mooly Sagiv, Eran Yahav
      Pages 477-490

About these proceedings


This volume contains the proceedings of the International Conference on C- puter Aided Veri?cation (CAV), held in Berlin, Germany, July 3–7, 2007. CAV 2007 was the 19th in a series of conferences dedicated to the advancement of the theory and practice of computer-assisted formal analysis methods for software and hardware systems. The conference covers the spectrum from theoretical - sults to concrete applications, with an emphasis on practical veri?cation tools and the algorithms and techniques that are needed for their implementation. We received 134 regular paper submissions and 39 tool paper submissions. Of these, the ProgramCommittee selected 33 regularpapersand 14 toolpapers. Each submission was reviewed by at least three members of the Program C- mittee. The reviewing process included a PC review meeting, and – for the ?rst time in the history of CAV – an author feedback period. About 50 additional reviews were provided by experts external to the Program Committee to assure a high quality selection. The CAV 2007 program included three invited talks from industry: – Byron Cook (Microsoft Research) on Automatically Proving Program T- mination, – David Russino? (AMD) on A Mathematical Approach to RTL Veri?cation, and – Thomas Kropf (Bosch) on Software Bugs Seen from an Industrial Persp- tive.


Erfüllbarkeitsproblem der Aussagenlogik Java algorithms automata automated deduction computational logic computer aided verification formal method formal methods formal program analysis formal verification model checking probabilistic verification reactive desi verification

Bibliographic information

  • DOI
  • Copyright Information Springer-Verlag Berlin Heidelberg 2007
  • Publisher Name Springer, Berlin, Heidelberg
  • eBook Packages Computer Science Computer Science (R0)
  • Print ISBN 978-3-540-73367-6
  • Online ISBN 978-3-540-73368-3
  • Series Print ISSN 0302-9743
  • Series Online ISSN 1611-3349
  • Buy this book on publisher's site
Industry Sectors
Finance, Business & Banking
IT & Software
Consumer Packaged Goods