Program Chairs
Kousha Etessami
University of Edinburgh
kousha@inf.ed.ac.uk
Sriram Rajamani
Microsoft Research
sriram@microsoft.com

Program Committee
Rajeev Alur, U. Penn
Thomas Ball, Microsoft Research
Alessandro Cimatti, IRST, Trento
Edmund R. Clarke, CMU
E. Allen Emerson, UT Austin
Kousha Etessami, U. Edinburgh
Patrice Godefroid, Bell Labs
Susanne Graf, Verimag
Orna Grumberg, Technion
Nicolas Halbwachs, Verimag
John Hatcliff, Kansas State U.
Thomas A. Henzinger, EPFL
Gerard J. Holzmann, NASA/JPL
Somesh Jha, U. of Wisconsin
Robert B. Jones, Intel Corp.
Orna Kupferman, Hebrew U.
Bob Kurshan, Cadence
Daniel Kroening, CMU
Marta Kwiatowska, U. of Birmingham
Rupak Majumdar, UCLA
Sharad Malik, Princeton U.
Ken McMillan, Cadence
Kedar Namjoshi, Bell Labs
John O'Leary, Intel
Madhusudan Parthasarathy, U. Illinois-Urbana
Doron Peled, U. Warwick
Sriram Rajamani, Microsoft Research
Jakob Rehof, Microsoft Research
Harald Ruess, SRI
Mooly Sagiv, Tel Aviv
Stefan Schwoon, U Stuttgart
Ofer Strichman, Technion
Helmut Veith, TU Munich
Thomas Wilke, Kiel U.
Yaron Wolfsthal, IBM Haifa
Yunshan Zhu, Synopsys

Steering Committee
Edmund M. Clarke, CMU
Mike Gordon, U of Cambridge
Robert P. Kurshan, Cadence
Amir Pnueli, NYU

Aims and Scope. CAV'05 conference is the 17th in a series 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 results to concrete applications, with an emphasis on practical verification tools and the algorithms and techniques that are needed for their implementation. The proceedings of the conference will be published in the Springer-Verlag Lecture Notes in Computer Science series. Sample topics of interest include:

• Algorithms and tools for verifying models and implementations
  
• Deductive, compositional, and abstraction techniques for verification
  
• Modeling and specification formalisms
  
• Program analysis and software verification
  
• Testing and runtime analysis based on verification technology
  
• Applications and case studies
  
• Verification in industrial practice

Invited Speakers:

• Bob Bentley(Intel),
  "Validating a modern microprocessor."
• Bud Mishra (NYU),
  ""What's Next? Challenges from Systems Biology."
• George Necula (U.C. Berkeley),
  "Randomized algorithms for program analysis and verification."

Tutorials:

• Tutorial on Automated abstraction refinement ,
  by Thomas Ball (Microsoft) & Ken McMillan (Cadence).
• Tutorial on Theory & practice of decision procedures for combinations of (first-order) theories,
  by Clark Barrett (NYU) and Cesare Tinelli (U. Iowa).

Satellite Events (July 11-12th):

• BMC'05: 3rd Int. Workshop on Bounded Model Checking. Organizers: A. Biere & O. Strichman.
• FATES'05: 5th Workshop on Formal Approaches to Testing Software, Organizers: W. Grieskamp & C. Weise.
• GDV'05: 2nd Workshop on Games in Design and Verification. Organizers: M. Jurdzinski & R. Majumdar.
• PDPAR'05: 3rd Workshop on Pragmatics of Decision Procedures in Automated Reasoning. Organizers: A. Armando & A. Cimatti.
• RV'05: 5th Workshop on Runtime verification,
  Organizers: H. Barringer, B. Finkbeiner, Y. Gurevich, & H. Sipma.
• SoftMC'05: 3rd Workshop on Software Model Checking. Organizers: B. Cook, S. Stoller, & W. Visser.
• "Satisfiability Modulo Theories Competition", a special tools competition. Organizers: C. Barrett, L. Demoura & A. Stump.

Paper submission. There are two categories of submissions:

A. Regular papers. Submissions should be in PS or PDF format, should not exceeding thirteen (13) pages and should use Springer's LNCS format with STANDARD margins. An additional clearly marked appendix may be included with the submission, but will only be read at the discretion of the program committee. Submissions deviating from these guidelines risk summary rejection. Submissions should contain original research, and sufficient detail to assess the merits and relevance of the contribution. For papers reporting experimental results, authors are strongly encouraged to make their data available with their submission. Simultaneous submission to other conferences with proceedings or submission of material that has already been published elsewhere is strictly forbidden.

B. Tool presentations. Submissions, not exceeding four (4) pages using Springer's LNCS format with STANDARD margins, should describe the implemented tool and its novel features. An additional clearly marked appendix may be included with the submission, but will only be read at the discretion of the program committee. A demonstration is expected to accompany a tool presentation. Papers describing tools that have already been presented in this conference before will be accepted only if significant and clear enhancements to the tool are reported and implemented.

The only mechanism for paper submissions is via the electronic submission web site, accessible via the conference homepage.

Important dates.