26th International Conference on
Computer Aided Verification (CAV’14)
18-22 July 2014, Vienna, Austria

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.

These changes are explained in more detail 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 (, 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


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:


Deadlines are “anywhere on earth”

  • 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


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

David Monniaux, CNRS, Verimag, Grenoble, France
How do we get inductive invariants?

Invited Talks

Erik Winfree, Caltech, Pasadena, California, USA
Designing and verifying molecular circuits and systems made of DNA

Rance Cleaveland, Univ. Maryland and Fraunhofer, USA
will talk about Automated Testing (preliminary title)

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

The nominations should be sent to Martha Kwiatowska ( Nominations must be received by January 15, 2014.


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