[SMT-LIB] CAV 2014: First Call for Papers

[Martina Seidl]

First Call for Papers
26th International Conference on Computer Aided Verification (CAV’14)
Part of Vienna Summer of Logic (VSL'14)
18-22 July 2014, Vienna, Austria
http://www.cavconference.org

New Rules
---------

We will continue to have short and long papers, but
short papers are not restricted to be tool papers anymore.

Further, we particularly encourage to submit high
quality tool papers and empirical evaluations as long papers.

References do not count toward the page limit.

More details are explained below.


Aims and Scope
--------------

CAV 2014 is the 26th in a series dedicated to the advancement of the
theory and practice of computer-aided formal analysis methods for
hardware and software systems. As part of the Federated Logic
Conference (FloC) and the Vienna Summer of Logic (vsl2014.at), CAV14
will be collocated with many other conferences in logic. 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 but are not limited to:
--------------------------------------------------

   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


Events
------

FLOC will host CAV-related workshops on 17-18 July and on 23-24 July
and the first day of CAV will be dedicated to tutorials. Please see
the conference website for further details.


Paper Submission
----------------

Submissions should contain original research, and sufficient detail
to assess the merits and relevance of the contribution. We welcome
papers on theory, case studies and reproductions and comparisons of
existing experimental research, tool papers, as well as combinations
of new theory with experimental evaluation. In contrast to previous
years, we have decoupled paper length from paper topic: We welcome
both long tool papers and short papers of any kind.

Tool papers should describe system and implementation aspects of a
tool with a large (potential) user base (experiments not required,
rehash of theory strongly discouraged). 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. Submissions reporting on case studies in an industrial
context are strongly invited, and should describe details,
weaknesses, and strengths in sufficient depth. Papers reproducing and
comparing existing results experimentally do not require new
theoretical insights. Examples of contributions of such papers are
evaluations of existing results in a superior experimental setting
and comparisons of methods that have not previously been thoroughly
experimentally compared.

The authors of tool papers and papers with experimental evaluation
should make every effort to make results reproducible by submitting
through EasyChair a repository including the implementation in source
and binary as well as benchmarks and logfiles. If this is not
possible, the reasons should be explained in the paper.

Papers can be submitted in either a regular or a short format.

Regular Papers should not exceed 15 pages in LNCS format,
not counting references.

Short Papers should not exceed 6 pages, not counting references.
Short papers are encouraged for any subject that can be described
within the page limit, and in particular for novel ideas without an
extensive experimental evaluation. Short papers will be accompanied
by short presentations.

An appendix can provide 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. Papers will be accepted or rejected in the category in which
they were submitted, there will be no "demotions" from a regular to a
short paper.

Simultaneous submission to other conferences with proceedings or
submission of material that has already been published elsewhere is
not allowed.

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://www.cavconference.org.


Deadlines
---------

   Abstract submission: 31 January 2014

   Paper submission (firm): 7 February 2014

   Author feedback/rebuttal period: 20-23 March 2014

   Notification of acceptance/rejection: 18 April 2014

   Final version due: 9 May 2014


   (all deadlines are "anywhere on earth")


Tutorials
---------

   Fabio Somenzi, University of Colorado at Boulder, USA will give a
   tutorial on Hardware Model Checking.

   David Monniaux, CNRS, Verimag, Grenoble, France
   will give a tutorial on Abstract Interpretation.


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 2014 CAV Award Committee consists of

   Marta Kwiatkowska, Oxford University, UK, Chair

   Moshe Vardi, Rice University, USA

   Ahmed Bouajjani, University Paris Diderot, France

   Tom Ball, Microsoft, USA

The nominations should be sent to Martha Kwiatowska
(Marta.Kwiatkowska at cs.ox.ac.uk).

Nominations must be received by January 15, 2014.


Chairs
------

Armin Biere, Johannes Kepler University Linz, Austria
Roderick Bloem, Graz University of Technology, Austria


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

Rajeev Alur, University of Pennsylvania, USA
Domagoj Babic, Google, USA
Gogul Balakrishnan, NEC, USA
Armin Biere, Johannes Kepler University Linz, Austria
Nikolaj Bjorner, Microsoft Research, USA
Roderick Bloem, Graz University of Technology, Austria
Ahmed Bouajjani, University Paris Diderot, France
Aaron Bradley, Mentor Graphics, University of Colorado at Boulder, USA
Pavol Cerny, University of Colorado at Boulder, USA
Koen Claessen, Chalmers University of Technology, Sweden
Byron Cook, Microsoft and University College London, UK
Azadeh Farzan, University of Toronto, Canada
Bernd Finkbeiner, Saarland University, Germany
Jasmin Fisher, Microsoft, UK
Mike Gordon, University of Cambridge, UK
Orna Grumberg, Technion, Israel
Leopold Haller, Cadence, USA
Keijo Heljanko, Aalto University, Finland
William Hung, Synopsys, USA
Somesh Jha, University of Wisconsin, USA
Susmit Jha, Intel, USA
Barbara Jobstmann, EPFL, Jasper DA, and CNRS-Verimag, France
Bengt Jonsson, Uppsala University, Sweden
Laura Kovacs, Chalmers University of Technology, Sweden
Daniel Kroening, Oxford University, UK,
Marta Kwiatkowska, Oxford University, UK
Kim G. Larsen, Aalborg University, Denmark
Joao Marques-Silva, University College Dublin, Ireland
Kedar Namjoshi, Bell Labs, USA
Corina Pasareanu, CMU/NASA Ames Research Center, USA
Doron Peled, Bar Ilan University, Israel
Pavithra Prabhakar, IMDEA Software Institute, Spain
Jean-Francois Raskin, Université Libre de Bruxelles, Belgium
Koushik Sen, University of California, Berkeley, USA
Natasha Sharygina, Universita’ della Svizzera Italiana, Switzerland
Nishant Sinha, IBM, India
Anna Slobodova, Centaur Technology, USA
Fabio Somenzi, University of Colorado at Boulder, USA
Cesare Tinelli, The University of Iowa, USA
Thomas Wahl Northeastern University, USA
Georg Weissenbacher, Vienna University of Technology, Austria
Eran Yahav, Technion, Israel


Workshop / Competition Chair
----------------------------

Martina Seidl, Johannes Kepler University Linz, Austria


Publication Chair
-----------------

Swen Jacobs, Graz University of Technology, Austria


Steering Committee
-----------------

Michael Gordon, University of Cambridge, UK
Orna Grumberg, Technion, Israel
Aarti Gupta, NEC, USA
Kenneth McMillan, Microsoft, USA