Call for Papers

Aims and Scope

CAV'07 is the 19th 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, and maintain its recent momentum in software verification. 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 and 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

Invited Speakers

• Byron Cook, Microsoft Research
• David Russinoff, AMD
• Thomas Kropf, Robert Bosch AG

Events

This year, there will be eight affiliated workshops:

• AHA 07: International Symposium on Automatic Heap Analysis
• ARTIST Workshop on tool platforms for modelling, analysis and validation of embedded systems
• BMC 07: 5th International Workshop on Bounded Model Checking
• FMICS 2007: 12th Intl. Workshop on Formal Methods for Industrial Critical Systems
• GVD 2007: 3rd German Verification Day
• HW-MC-COMP: Hardware Model Checking Competition
• PDMC 07: 6th Int. Workshop on Parallel and Distributed Methods in verifiCation
• SMT 2007: 5th International Workshop on Satisfiability Modulo Theories
• SMT-COMP: Satisfiability Modulo Theories Tools Competition
• SPIN 2007: 14th International SPIN Workshop on Model Checking of Software

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.

Information concerning the procedure for submissions will be available on the conference home page:

http://www.cav2007.org


Papers exceeding the stated maximum length or submitted after January 28, 2007 run the risk of rejection without review.

On an experimental basis for this year, authors will be granted access to the text content of their reviews during the review process. Authors will be given a short time period in which to submit feedback, which may (at the PC's discretion) be taken into account in the decision process. Strict guidelines on length and content of feedback will be provided to the authors.

Important dates

• Paper submission (firm): January 28, 2007
• Author feedback period: March 9-11, 2007
• Notification of acceptance/rejection: March 23, 2007
• Final version due: April 20, 2007

Program Chairs

• Werner Damm, U Oldenburg, damm(at)informatik.uni-oldenburg.de
• Holger Hermanns, Saarland U, hermanns(at)cs.uni-sb.de

Program Committee

• Parosh Abdulla, Uppsala U
• Rajeev Alur, U Penn
• Sergey Berezin, Synopsys
• Armin Biere, JKU Linz
• Roderick Bloem, TU Graz
• Ahmed Bouajjani, U Paris 7
• Alessandro Cimatti, IRST Trento
• Edmund M. Clarke, CMU
• Werner Damm, U Oldenburg
• Limor Fix, Intel
• Patrice Godefroid, Microsoft Research
• Ganesh Gopalakrishnan, U of Utah
• Susanne Graf, Verimag
• Orna Grumberg, Technion
• Holger Hermanns, Saarland U
• Robert Jones, Intel
• Orna Kupferman, Hebrew U
• Robert P. Kurshan, Cadence
• John Lygeros, ETH Zuerich
• Tom Melham, Oxford U
• Ken McMillan, Cadence
• Jakob Rehof, U Dortmund
• Koushik Sen, UC Berkeley
• Fabio Somenzi, U Boulder
• Ashish Tiwari, SRI International
• Frits Vaandrager, U Nijmegen
• Yaron Wolfstal, IBM Haifa

Steering Committee

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