Computer Aided Verification

17th International Conference, CAV 2005, Edinburgh, Scotland, UK, July 6-10, 2005. Proceedings

  • Kousha Etessami
  • Sriram K. Rajamani
Conference proceedings CAV 2005

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

Table of contents

  1. Front Matter
  2. Invited Talks

    1. George C. Necula, Sumit Gulwani
      Pages 1-1
    2. Bob Bentley
      Pages 2-4
    3. C. Piazza, M. Antoniotti, V. Mysore, A. Policriti, F. Winkler, B. Mishra
      Pages 5-19
  3. Tools Competition

    1. Clark Barrett, Leonardo de Moura, Aaron Stump
      Pages 20-23
  4. Abstraction and Refinement

    1. Shuvendu K. Lahiri, Thomas Ball, Byron Cook
      Pages 24-38
    2. Ranjit Jhala, K. L. McMillan
      Pages 39-51
    3. Corina S. Păsăreanu, Radek Pelánek, Willem Visser
      Pages 52-66
    4. Thomas Ball, Orna Kupferman, Greta Yorsh
      Pages 67-81
  5. Bounded Model Checking

    1. Ishai Rabinovitz, Orna Grumberg
      Pages 82-97
    2. Keijo Heljanko, Tommi Junttila, Timo Latvala
      Pages 98-111
    3. Anubhav Gupta, Ofer Strichman
      Pages 112-124
    4. Daijue Tang, Sharad Malik, Aarti Gupta, C. Norris Ip
      Pages 125-138
  6. Tool Papers I

    1. Yichen Xie, Alex Aiken
      Pages 139-143
    2. Ajay Chander, David Espinosa, Nayeem Islam, Peter Lee, George Necula
      Pages 144-147
    3. Matthew B. Dwyer, John Hatcliff, Matthew Hoosier, Robby
      Pages 148-152
    4. Sharon Barner, Ziv Glazberg, Ishai Rabinovitz
      Pages 153-157
    5. G. Balakrishnan, T. Reps, N. Kidd, A. Lal, J. Lim, D. Melski et al.
      Pages 158-163
    6. Sagar Chaki, James Ivers, Natasha Sharygina, Kurt Wallnau
      Pages 164-169
  7. Verification of Hardware, Microcode, and Synchronous Systems

    1. Tamarah Arons, Elad Elster, Limor Fix, Sela Mador-Haim, Michael Mishaeli, Jonathan Shalev et al.
      Pages 185-198
  8. Games and Probabilistic Verification

    1. Barbara Jobstmann, Andreas Griesmayer, Roderick Bloem
      Pages 226-238
    2. Amitabha Roy, K. Gopinath
      Pages 239-252
    3. Håkan L. S. Younes
      Pages 253-265
    4. Koushik Sen, Mahesh Viswanathan, Gul Agha
      Pages 266-280
  9. Tool Papers II

    1. A. Armando, D. Basin, Y. Boichut, Y. Chevalier, L. Compagna, J. Cuellar et al.
      Pages 281-285
    2. Julien Olivain, Jean Goubault-Larrecq
      Pages 286-290
    3. Clark Barrett, Yi Fang, Benjamin Goldberg, Ying Hu, Amir Pnueli, Lenore Zuck
      Pages 291-295
    4. Byron Cook, Daniel Kroening, Natasha Sharygina
      Pages 296-300
    5. F. Ivančić, Z. Yang, M. K. Ganai, A. Gupta, I. Shlyakhter, P. Ashar
      Pages 301-306
  10. Decision Procedures and Applications

    1. Orly Meir, Ofer Strichman
      Pages 307-320
    2. Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi Junttila, Silvio Ranise, Peter van Rossum et al.
      Pages 335-349
  11. Automata and Transition Systems

    1. Roberto Sebastiani, Stefano Tonetta, Moshe Y. Vardi
      Pages 350-363
    2. Marcelo d’Amorim, Grigore Roşu
      Pages 364-378
    3. Michael Benedikt, Angela Bonifati, Sergio Flesca, Avinash Vyas
      Pages 379-393
    4. Gilles Geeraerts, Jean-François Raskin, Laurent Van Begin
      Pages 394-407
  12. Tool Papers III

    1. Ittai Balaban, Yi Fang, Amir Pnueli, Lenore D. Zuck
      Pages 408-412
    2. Tuba Yavuz-Kahveci, Constantinos Bartzis, Tevfik Bultan
      Pages 413-417
    3. Guillaume Gardey, Didier Lime, Morgan Magnin, Olivier (H. ) Roux
      Pages 418-423
    4. Enric Pastor, Marco A. Peña, Marc Solé
      Pages 424-428
    5. Håkan L. S. Younes
      Pages 429-433
  13. Program Analysis and Verification I

    1. Akash Lal, Thomas Reps, Gogul Balakrishnan
      Pages 434-448
    2. Christopher L. Conway, Kedar S. Namjoshi, Dennis Dams, Stephen A. Edwards
      Pages 449-461
    3. A. Costan, S. Gaubert, E. Goubault, M. Martel, S. Putot
      Pages 462-475
  14. Program Analysis and Verification II

    1. Scott McPeak, George C. Necula
      Pages 476-490
    2. Aaron R. Bradley, Zohar Manna, Henny B. Sipma
      Pages 491-504
    3. Vineet Kahlon, Franjo Ivančić, Aarti Gupta
      Pages 505-518

About these proceedings


This volume contains the proceedings of the International Conference on Computer Aided Veri?cation (CAV), held in Edinburgh, Scotland, July 6–10, 2005. CAV 2005 was the seventeenth in a series of conferences dedicated to the advancement of the theory and practice of computer-assisted formal an- ysis methods for software and hardware systems. The conference covered the spectrum from theoretical results to concrete applications, with an emphasis on practical veri?cation tools and the algorithms and techniques that are needed for their implementation. We received 123 submissions for regular papers and 32 submissions for tool papers.Ofthesesubmissions,theProgramCommitteeselected32regularpapers and 16 tool papers, which formed the technical program of the conference. The conference had three invited talks, by Bob Bentley (Intel), Bud Mishra (NYU), and George C. Necula (UC Berkeley). The conference was preceded by a tutorial day, with two tutorials: – Automated Abstraction Re?nement, by Thomas Ball (Microsoft) and Ken McMillan (Cadence); and – Theory and Practice of Decision Procedures for Combinations of (First- Order) Theories, by Clark Barrett (NYU) and Cesare Tinelli (U Iowa). CAV 2005 had six a?liated workshops: – BMC 2005: 3rd Int. Workshop on Bounded Model Checking; – FATES 2005: 5th Workshop on Formal Approaches to Testing Software; – GDV 2005: 2nd Workshop on Games in Design and Veri?cation; – PDPAR 2005: 3rd Workshop on Pragmatics of Decision Procedures in - tomated Reasoning; – RV 2005: 5th Workshop on Runtime Veri?cation; and – SoftMC 2005: 3rd Workshop on Software Model Checking.


Compiler Erfüllbarkeitsproblem der Aussagenlogik Syntax algorithms automata automated deduction computational logic computer aided verification formal methods formal program analysis formal verification hardware verification microprocessor petri net verification

Editors and affiliations

  • Kousha Etessami
    • 1
  • Sriram K. Rajamani
    • 2
  1. 1.LFCS, School of InformaticsUniversity of Edinburgh 
  2. 2.Microsoft Research India 

Bibliographic information

Industry Sectors
IT & Software