20th International Conference on
		Computer Aided Verification (CAV)
                         CAV 2008
            http://www.princeton.edu/cav2008

                     July 7 - 14, 2008
                      Princeton, USA

                 Second Call for Papers
........................................................................

Aims and Scope
----------------------
CAV 2008 is the 20th in a series dedicated to the advancement of the
theory and practice of computer-aided formal analysis methods for
hardware and software systems. CAV considers it vital to continue its
leadership in hardware verification, maintain its recent momentum in
software verification, and consider new domains such as biological
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. A
selection of papers will be invited to a special issue of the
International Journal on Formal Methods in System Design. 

Topics of interest include:
  * Algorithms and tools for verifying models and implementations
  * Hardware verification techniques
  * Hybrid systems and embedded systems verification
  * Program analysis and software verification
  * Modeling and specification formalisms
  * Deductive, compositional, and abstraction techniques for
verification
  * Testing and runtime analysis based on verification technology
  * Applications and case studies
  * Verification in industrial practice 
  * Formal methods for biological systems (new this year)

Events
----------
There will be pre-conference workshops on July 7 and July 8, and
post-conference workshops on July 14. Please see the conference website
for more details.

There will be tutorials on July 9 (first day of the conference). 
Invited tutorial speakers: 
 * Harry Foster (Mentor Graphics)
 * John Harrison (Intel)
 * Peter O' Hearn (Queen Mary, University of London)
 * Reinhard Wilhelm (Saarland University)

CAV Award
-------------
An annual award, called the CAV Award, has been established
       "For a specific fundamental contribution
       or a series of outstanding contributions
       to the field of Computer-Aided Verification."

The cited contribution(s) must have been made not more recently than
five years ago and not over twenty years ago.  In addition, the
contribution(s) should not yet have received recognition via a major
award, such as the ACM Turing or Kanellakis Awards. (The nominee may
have received such an award for other contributions.)

The award of ,000 will be granted to an individual or a group of
individuals chosen by the Award Committee from a list of nominations.
The Award Committee may choose to make no award in a given year.

The CAV Award will be presented in an award ceremony at the
Computer-Aided Verification Conference and a citation will be published
in a journal of record (currently, Formal Methods in System Design).

Anyone, with the exception of members of the Award Committee, is
eligible to receive the Award.

Please see the Call for Nominations for the CAV Award on the conference
website.

Paper Submission
-------------------------
There are two categories of submissions: 

* A. Regular papers. Submissions, not exceeding thirteen (13) pages
using Springer's LNCS format, 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.
Submissions reporting on case studies in an industrial context are
strongly invited, and should describe details, weaknesses and strength
in sufficient depth. Simultaneous submission to other conferences with
proceedings or submission of material that has already been published
elsewhere is not allowed.

* B. Tool presentations. Submissions, not exceeding four (4) pages using
Springer's LNCS format, should describe the implemented tool and its
novel features. 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.

Papers can be submitted in PDF or PS format. Submission is done with
EasyChair, and the submission site will open on Jan 7, 2008. Please
follow guidelines on the conference website:
http://www.princeton.edu/cav2008 .

Papers exceeding the stated maximum length run the risk of rejection
without review. The review process will include a feedback/rebuttal
period where authors will have the option to respond to reviewer
comments. 

Important Dates 
-----------------------
  * Paper submission (firm): January 28, 2008
  * Author feedback/rebuttal period: March 9-11, 2008
  * Notification of acceptance/rejection: March 26, 2008
  * Final version due: April 21, 2008

Program Chairs
----------------------
  * Aarti Gupta, NEC Labs America, agupta(at)nec-labs.com
  * Sharad Malik, Princeton University, sharad(at)princeton.edu

Program Committee
-----------------------------
  * Rajeev Alur, U Penn
  * Nina Amla, Cadence
  * Clark Barrett, NYU
  * Armin Biere, JKU Linz
  * Roderick Bloem, TU Graz
  * Ahmed Bouajjani, U Paris 7
  * Alessandro Cimatti, IRST Trento
  * Werner Damm, U Oldenburg
  * Steven German, IBM 
  * Ganesh Gopalakrishnan, U of Utah
  * Mike Gordon, U of Cambridge
  * Orna Grumberg, Technion
  * Aarti Gupta (co-chair), NEC Labs America
  * David Harel, Weizmann Institute
  * John Harrison, Intel
  * Tom Henzinger, EPFL
  * Holger Hermanns, Saarland U
  * Pei-Hsin Ho, Synopsys
  * Robert Jones, Intel
  * Daniel Kroening, Oxford U
  * Orna Kupferman, Hebrew U
  * Shuvendu Lahiri, Microsoft Research
  * Rupak Majumdar, UCLA
  * Oded Maler, Verimag
  * Sharad Malik (co-chair), Princeton U
  * Ken McMillan, Cadence
  * Kedar Namjoshi, Bell Labs, Alcatel-Lucent
  * Corina Pasareanu, NASA
  * Amir Pnueli, NYU
  * Andreas Podelski, U of Freiburg
  * Shaz Qadeer, Microsoft Research
  * Koushik Sen, UC Berkeley
  * Fabio Somenzi, U of Colorado at Boulder
  * Ofer Strichman, Technion
  * Karen Yorav, IBM Haifa
  * Lenore Zuck, U of Illinois at Chicago

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