22nd International Conference on Computer Aided Verification (CAV)

CAV 2010

July 15 - 19, 2010
Edinburgh, United Kingdom

http://www.liafa.jussieu.fr/~touili/cav2010/

Call for Papers

Aims and Scope

CAV 2010 is the 22nd in a series dedicated to the advancement of the theory and practice of computer-aided formal analysis methods for hardware and software systems. This year, CAV is part of the 5th International Federated Logic Conference (FLoC 2010), which includes CAV and seven other conferences/symposia: CSF, ICLP, IJCAR, ITP, LICS, RTA and SAT.

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:

• Model checking techniques
• 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

Events

There will be pre-conference workshops on July 14 and July 15, and post-conference workshops on July 20. Details on affiliated workshops can be found on the conference website.

There will be tutorials on July 15 (first day of the conference).

Invited tutorial speakers

Robert Brayton, University of California, Berkeley, US
Kenneth Mcmillan, Cadence Berkeley Labs, US
Thomas Reps, University of Wisconsin-Madison, US
Andrey Rybalchenko, Max Planck Institute, Germany

Invited speakers

Somesh Jha, University of Wisconsin-Madison, US
Pasquale Malacaria, Queen Mary University, United Kingdom
Maged Michael, IBM, US

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 $10,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.

Nominations are welcome. Details on how to make a nomination can be found on the conference website.

Paper Submission

There are two categories of submissions:

• A. Regular papers. Submissions, not exceeding fourteen (14) 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 4, 2010.

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

• Abstract submission: January 11, 2010
• Paper submission (firm): January 17, 2010
• Author feedback/rebuttal period: February 26 - March 1, 2010
• Notification of acceptance/rejection: March 15, 2010
• Final version due: April 16, 2010

Program Chairs

Byron Cook, Microsoft Research, United Kingdom
Paul Jackson, University of Edinburgh, United Kingdom
Tayssir Touili, LIAFA-CNRS, France

Program Committee

Rajeev Alur, University of Pennsylvania, US
Domagoj Babic, Synopsys, US
Christel Baier, Technical University of Dresden, Germany
Roderick Bloem, Graz University of Technology, Austria
Ahmed Bouajjani, LIAFA-University of Paris 7, France
Alessandro Cimatti, FBK-irst, Italy
Byron Cook, Microsoft Research, United Kingdom
Javier Esparza, Technische Universität München, Germany
Azadeh Farzan, University of Toronto, Canada
Martin Fränzle, University of Oldenburg, Germany
Ganesh Gopalakrishnan, University of Utah, US
Mike Gordon, University of Cambridge, United Kingdom
Orna Grumberg, Technion, Israel
Ziyad Hanna, Jasper, US
Holger Hermanns, Saarland University, Germany
Alan Hu, University of British Columbia, Canada
Paul Jackson, University of Edinburgh, United Kingdom
Kevin Jones, Green Plug, US
Vineet Kahlon, NEC Labs, US
Jean Krivine, PPS-CNRS, France
Daniel Kroening, Oxford University, United Kingdom
Sava Krstic, Intel Corporation, US
Marta Kwiatkowska, Oxford University, United Kingdom
Oded Maler, VERIMAG-CNRS, France
Kenneth McMillan, Cadence, US
David Monniaux, VERIMAG-CNRS, France
Markus Müller-Olm, Muenster University, Germany
Kedar Namjoshi, Bell Labs, US
Doron Peled, Bar Ilan University, Israel
Shaz Qadeer, Microsoft Research, US
Jean-Francois Raskin, Brussels University, Belgium
Natasha Sharygina, University of Lugano, Switzerland
Tayssir Touili, LIAFA-CNRS, France
Helmut Veith, University of Darmstadt, Germany
Kwangkeun Yi, Seoul National University, Korea
Karen Yorav, IBM Haifa, Israel
Greta Yorsh, IBM, US

Steering Committee

Edmund M. Clarke, Carnegie Mellon University, US
Mike Gordon, University of Cambridge, United Kingdom
Orna Grumberg, Technion, Israel
Robert P. Kurshan, Cadence, US
Kenneth McMillan, Cadence, US

Workshop Chair