====== CALL FOR PAPERS =====
25th International Conference on Computer Aided Verification (CAV
2013) July 13-19, 2013 St. Petersburg, Russia

Program Chairs: Natasha Sharygina and Helmut Veith
Website: http://cav2013.forsyte.at/

Aims and Scope
-------------------
The conference on Computer Aided Verification (CAV), 2013, is the 25th
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 spurring advances in
hardware and software verification while expanding to new domains such
as biological systems and computer security. 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 Formal Methods in System Design and the
Journal of the ACM.

Topics of interest include:
- Algorithms and tools for verifying models and implementations
- Hardware verification techniques
- Deductive, compositional, and abstraction techniques for verification
- Program analysis and software verification
- Verification methods for parallel and concurrent hardware/software systems
- Testing and runtime analysis based on verification technology
- Applications and case studies in verification
- Decision procedures and solvers for verification
- Mathematical and logical foundations of practical verification tools
- Verification in industrial practice
- Algorithms and tools for system synthesis
- Hybrid systems and embedded systems verification
- Verification techniques for security
- Formal models and methods for biological systems

Following the example of 2012, CAV will again have *special tracks* in
four areas:

1. Hardware Verification (track chair: Armin Biere)
2. Computer Security (track chair: Somesh Jha)
3. SAT and SMT (track chair: Nikolaj Bjoerner)
4. Biology (track chair: Jasmin Fisher)

Submissions in these four topics are especially encouraged. Papers in
these areas will be subject to the same rigorous review process as
other papers. Accepted special track papers will be organized into
special sessions that are highlighted in the program.

In addition, CAV 2013 will also have a track chair for tool papers:

5. Tool Papers (track chair: Roderick Bloem)

Events
---------
The conference will include the following events:
* Pre-conference workshops on July 13-14.
* The main conference will take place July 15th-19th:
* Invited tutorials on July 15th.
* Technical sessions on July 16-19.

Please see the conference website for further details.

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

A. Regular Papers: Submissions, not exceeding sixteen (16) 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 strengths in sufficient depth. Simultaneous submission to other
conferences with proceedings or submission of material that has
already been published elsewhere is not allowed. An appendix can be
joined to the submissions providing additional material such as
details on proofs or experiments. The appendix is not guaranteed to be
read or taken into account by the reviewers and it should not contain
information necessary to the understanding and the evaluation of the
presented work.

B. Tool Presentations: Submissions, not exceeding six (6) pages using
Springer's LNCS format, should describe the implemented tool, its
novel features, and possibly an experimental evaluation. A
demonstration, in a separate demonstration session, is expected to
accompany a tool presentation. Papers describing tools that have
already been presented (in any conference) will be accepted only if
significant and clear enhancements to the tool are reported and
implemented. We strongly encourage authors to make their tools and
benchmarks available with their submission.

Papers exceeding the stated maximum length run the risk of rejection
without review.

An appendix can be joined to the submissions providing additional
material such as details on proofs or experiments. The appendix is not
guaranteed to be read or taken into account by the reviewers and
should not contain information necessary to the understanding and the
evaluation of the presented work. Note that the page limit for
submissions has been increased to 16 pages including references.

The review process will include a feedback/rebuttal period where
authors will have the option to respond to reviewer comments.

Papers must be submitted in PDF format. Submission is done with
EasyChair. Information about the submission procedure will be
available at: http://cav2013.forsyte.at

Important Dates
- Abstract submission: January 3, 2013
- Paper submission (firm): January 7, 2013 anywhere on earth
- Author feedback/rebuttal period: February 20-22, 2013
- Notification of acceptance/rejection: March 6, 2013
- Final version due: April 6, 2013


Program Chairs
------------------
Natasha Sharygina, University of Lugano, Switzerland
Helmut Veith, Vienna University of Technology, Austria


Program Committee
---------------------

Rajeev Alur (Univ. Pennsylvania)
Domagoj Babic (UC Berkeley)
Armin Biere (JKU Linz)
Nikolaj Bjorner (Microsoft Research)
Roderick Bloem (TU Graz)
Ahmed Bouajjani (LIAFA, Univ. of Paris 7)
Aaron Bradley (CU Boulder)
Hana Chockler (IBM)
Byron Cook (Microsoft Research, Univ. College London)
Vincent Danos (The University of Edinburgh)
Anupam Datta (Carnegie Mellon Univ.)
Javier Esparza (TU Munich)
Azadeh Farzan (Univ. of Toronto)
Bernd Finkbeiner (Saarland Univ.)
Jasmin Fisher (Microsoft Research)
Radu Grosu (TU Vienna)
Ari Gurfinkel (Carnegie Mellon Univ.)
William Hung (Synopsys Inc)
Susmit Jha (Intel)
Somesh Jha (Univ. of Wisconsin)
Barbara Jobstmann (CNRS, Verimag, Jasper DA)
Bengt Jonsson (Uppsala Univ.)
Rajeev Joshi (NASA JPL)
Joost-Pieter Katoen (RWTH Aachen)
Robert P. Kurshan (Cadence Design Systems)
Benjamin Livshits (Microsoft Research)
Rupak Majumdar (Max Planck Institute)
Ken Mcmillan (Microsoft Research)
Kedar Namjoshi (Bell Labs)
Joel Ouaknine (Oxford Univ.)
Madhusudan Parthasarathy (Univ. of Illinois at Urbana-Champaign)
Corina Pasareanu (Carnegie Mellon Univ., NASA Ames)
Andreas Podelski (Univ. of Freiburg)
Natasha Sharygina (Univ. of Lugano)
Nishant Sinha (IBM)
Anna Slobodova (Centaur Technology)
Murali Talupur (Intel)
Stavros Tripakis (UC Berkeley)
Helmut Veith (TU Vienna)
Mahesh Viswanathan (Univ. of Illinois at Urbana-Champaign)
Thomas Wahl (Northeastern Univ.)
Georg Weissenbacher (TU Vienna)
Eran Yahav (Technion)


Steering Committee
----------------------
Michael Gordon, University of Cambridge, UK
Orna Grumberg, Technion, Israel
Robert Kurshan, Cadence Design Systems, USA
Kenneth McMillan, Microsoft Research, USA

CAV Award
------------
The annual CAV Award has been established for a specific fundamental
contribution or a series of outstanding contributions to the field of
Computer Aided Verification. 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. The CAV Award shall be presented in an award ceremony at CAV
and a citation will be published in a Journal of Record (currently,
Formal Methods in System Design).

Call for Nominations for the CAV Award
------------------------------------------
Anyone can submit a nomination. The Award Committee can originate a
nomination. Anyone, with the exception of members of the Award
Committee, is eligible to receive the Award. A nomination must state
clearly the contribution(s), explain why the contribution is
fundamental or the series of contributions is outstanding, and be
accompanied by supporting letters and other evidence of worthiness.
Nominations should include a proposed citation (up to 25 words), a
succinct (100-250 words) description of the contribution(s), and a
detailed statement to justify the nomination. 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 2013 CAV Award Committee consists of
Rajeev Alur (Chair)
Marta Kwiatkowska
Aarti Gupta
Ahmed Bouajjani

The nominations should be sent to Rajeev Alur at alur@seas.upenn.edu.
Nominations must be received by January 7, 2013.