From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id 483217FA5F for ; Wed, 18 Jan 2017 13:37:02 +0100 (CET) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=mikael.mayer@epfl.ch; spf=Pass smtp.mailfrom=mikael.mayer@epfl.ch; spf=None smtp.helo=postmaster@smtp5.epfl.ch Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of mikael.mayer@epfl.ch) identity=pra; client-ip=128.178.224.8; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="mikael.mayer@epfl.ch"; x-sender="mikael.mayer@epfl.ch"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of mikael.mayer@epfl.ch designates 128.178.224.8 as permitted sender) identity=mailfrom; client-ip=128.178.224.8; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="mikael.mayer@epfl.ch"; x-sender="mikael.mayer@epfl.ch"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@smtp5.epfl.ch) identity=helo; client-ip=128.178.224.8; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="mikael.mayer@epfl.ch"; x-sender="postmaster@smtp5.epfl.ch"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3Aha0wWh0oTru0qC3YsmDT+DRfVm0co7zxezQtwd8Z?= =?us-ascii?q?seIQKvad9pjvdHbS+e9qxAeQG96Kt7Qf2qGK6+jJYi8p2d65qncMcZhBBVcuqP?= =?us-ascii?q?49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6?= =?us-ascii?q?JvjvGo7Vks+7y/2+94fdbghMizexe71/IRG5oQjeqsUdnJdvJLs2xhbVuHVDZv?= =?us-ascii?q?5YxXlvJVKdnhb84tm/8Zt++ClOuPwv6tBNX7zic6s3UbJXAjImM3so5MLwrhnM?= =?us-ascii?q?URGP5noHXWoIlBdDHhXI4wv7Xpf1tSv6q/Z91SyHNsD4Ubw4RTKv5LptRRT1ii?= =?us-ascii?q?kIKiQ5/XnYhcxrjKxUohyhqRJ8zYDJfo+aKOFzcbnBcd4AX2dNQtpdWi5HD4ih?= =?us-ascii?q?b4UPFe0BPeNAoon4plsOrgGxCheoBO/1zz9HnH/30rMg0+k6Dw7GxAIgH9YUvH?= =?us-ascii?q?vIrNX4MroZX+6yzKnN1zrDbvVW1C/46IjQcxAtuOqMXLxrccbLzkkvDQzFgk2M?= =?us-ascii?q?poP/ITOayuMNs26V7+V+T+KglWgnpB1vrTS1wccskIbJipoLylDF7yV53Js1Ks?= =?us-ascii?q?e8SEFgZt6lH4FctyaAN4t5Ws8iQ31ouDoiyr0CuJ67eisKyIgnxx7FbPyHboeI?= =?us-ascii?q?4hLkVOaMPTd4mHJld6yhiBas60egzvD8WdOo0FZLqSpFlMHMtmoK1xPP9MeHUe?= =?us-ascii?q?B98l271jaU0Q3Y9+JKIVgsmKbGNZIswaQ8mocRvEnABCP6hlv6gaCMekgn4uSk?= =?us-ascii?q?9fjrb7H8qpKfN4J4kB/yPrkhl8ClDuk1Mg4DVHWB9+umzr3s50j5Ta1KjvIolq?= =?us-ascii?q?nZt4jXJd8epq6lGw9Y0pwv5AinDzeo1NQUh2UILFJddBKGiYjmJU3OLejlAfuh?= =?us-ascii?q?gFmgiipnyvLFM7H7HJnBMHfOnK3icLpl7k5T0gszzdRR55JODbEBJer+WkrwtN?= =?us-ascii?q?zbFBA2LQi0z/ziCNpn1oIRR3iPD7SHP6PKv1+I4vgjLPWMZIMNojbyN+Al5+Ly?= =?us-ascii?q?jX8+gVISYbOm3Z4TaHyhGvRmIl6ZYWb3j9caEWYKuxI+Q/bwhF2DVz5TfXeyUL?= =?us-ascii?q?gm6jE1EoL1RbvEE4ukhbjE2CagArVXYHpHAxaCCyTGbYKBDvINayufJolkmy0J?= =?us-ascii?q?T5CsU4Elkxqu51yy8KZuMueBon5QjpnkztUgv+A=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0AeAACOYH9YhwjgsoBTChwBBQELARgBB?= =?us-ascii?q?QELAYMADwEBAQEBfoEJg1GKCJRikkyCCyaCRoM2AhUvgSc/GAEBAQEBAQEBAQE?= =?us-ascii?q?BEgEBAQoLCQodMIIzGYIeBhoDBkUDHgEIDQUoCgICIhIBBQEcIYh7kgiRDD+MA?= =?us-ascii?q?4IliigBAQEBAQUBAQEBAQEBAQEfjHWCZQQBgymCXgWJD4YYfkiKVIZfiwOBd1G?= =?us-ascii?q?EPYNNhhuFXYRghmwygRQPEIJfBYQrBIIJVYZEASWCFwEBAQ?= X-IPAS-Result: =?us-ascii?q?A0AeAACOYH9YhwjgsoBTChwBBQELARgBBQELAYMADwEBAQE?= =?us-ascii?q?BfoEJg1GKCJRikkyCCyaCRoM2AhUvgSc/GAEBAQEBAQEBAQEBEgEBAQoLCQodM?= =?us-ascii?q?IIzGYIeBhoDBkUDHgEIDQUoCgICIhIBBQEcIYh7kgiRDD+MA4IliigBAQEBAQU?= =?us-ascii?q?BAQEBAQEBAQEfjHWCZQQBgymCXgWJD4YYfkiKVIZfiwOBd1GEPYNNhhuFXYRgh?= =?us-ascii?q?mwygRQPEIJfBYQrBIIJVYZEASWCFwEBAQ?= X-IronPort-AV: E=Sophos;i="5.33,249,1477954800"; d="scan'208,217";a="209738669" Received: from smtp5.epfl.ch ([128.178.224.8]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 18 Jan 2017 13:37:00 +0100 Received: (qmail 23961 invoked by uid 107); 18 Jan 2017 12:36:53 -0000 X-Virus-Scanned: ClamAV Received: from mail-it0-f45.google.com (HELO mail-it0-f45.google.com) (209.85.214.45) (TLS, DHE-RSA-AES256-SHA cipher) (authenticated) by mail.epfl.ch (AngelmatoPhylax SMTP proxy) with ESMTPSA; Wed, 18 Jan 2017 13:36:54 +0100 Received: by mail-it0-f45.google.com with SMTP id 203so116362821ith.0 for ; Wed, 18 Jan 2017 04:36:53 -0800 (PST) X-Gm-Message-State: AIkVDXLJF25SA7DpRsflaZYKgPk0DVUF2RKTvFHKIG0jhJn6XH0cpTMNdSoi11RB/u6ksHorKkSGGz8ToDLVKg== X-Received: by 10.36.153.197 with SMTP id a188mr9920386ite.5.1484743011582; Wed, 18 Jan 2017 04:36:51 -0800 (PST) Received: from 1074892088431 named unknown by gmailapi.google.com with HTTPREST; Wed, 18 Jan 2017 07:36:51 -0500 MIME-Version: 1.0 Sender: mikael.mayer@epfl.ch From: mikael.mayer@epfl.ch In-Reply-To: References: Date: Wed, 18 Jan 2017 07:36:51 -0500 X-Google-Sender-Auth: v-jcfFntBLUAVlHMY6MW4e4fSpA X-Gmail-Original-Message-ID: Message-ID: To: caml-list@inria.fr Content-Type: multipart/alternative; boundary=94eb2c0895b4c9ceab05465dab21 X-Validation-by: mikael.mayer@epfl.ch Subject: [Caml-list] CAV 2017: Call for Papers --94eb2c0895b4c9ceab05465dab21 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable CAV 2017: 29th International Conference on Computer-Aided Verification Important Dates: All deadlines are AOE (Anywhere on Earth). Papers: Paper submission: January 24, 2017 (Tuesday) Author response period: March 20-22, 2017 (Monday =E2=80=93 Wednesday) Author notification: April 12, 2017 (Wednesday) Final version: May 5, 2017 (Friday) Conference: Workshops: July 22-23, 2017 Main conference: July 24-28, 2017 Submission URL http://cav2017.mpi-sws.org/ Scope CAV 2017 is the 29th in a series dedicated to the advancement of the theory and practice of computer-aided formal analysis and synthesis methods for hardware and software systems. CAV considers it vital to continue spurring advances in hardware and software verification while expanding to domains such as cyber-physical, social, and 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 LNCS 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 Algorithms and tools for system synthesis Mathematical and logical foundations of verification and synthesis Specifications and correctness criteria for programs and systems Deductive verification using proof assistants Hardware verification techniques Program analysis and software verification Software synthesis Hybrid systems and embedded systems verification Compositional and abstraction-based techniques for verification Probabilistic and statistical approaches to verification Verification methods for parallel and concurrent systems Testing and run-time analysis based on verification technology Decision procedures and solvers for verification and synthesis Applications and case studies in verification and synthesis Verification in industrial practice New application areas for algorithmic verification and synthesis Formal models and methods for security Formal models and methods for biological systems Paper Submission NEW this year: There is no separate registration deadline. Full papers should be uploaded by the submission deadline. Tool papers require a concurrent artifact submission together with the paper submission. Artifact evaluation occurs concurrently with the review process and the PC gets access to the artifact evaluation during the PC discussions. Submissions on a wide range of topics are sought, particularly ones that identify new research directions. CAV 2017 is not limited to topics discussed in previous instances of the conference. Authors concerned about the appropriateness of a topic may communicate with the conference chairs prior to submission. As explained below, CAV 2017 will follow a lightweight double-blind review process. Submissions that are not =E2=80=9Cblinded=E2=80=9D will be reject= ed without review. 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. The PC chairs may solicit further reviews after the rebuttal period. Papers must be submitted in PDF format here https://cav2017.mpi-sws.org/ Submissions will be in two categories: Regular Papers and Tool Papers. Regular Papers Regular Papers should not exceed 16 pages in LNCS format, not counting references and appendices. Authors can include a clearly marked appendix at the end of their submissions, that is exempt from the page limit restrictions. However, the reviewers are not obliged to read the contents of these appendices. These papers should contain original research and sufficient detail to assess the merits and relevance of the contribution. Papers will be evaluated on basis of a combination of correctness, technical depth, significance, novelty, clarity, and elegance. We welcome papers on theory, case studies, and comparisons with existing experimental research, as well as combinations of new theory with experimental evaluation. A strong theoretical paper is not required to have an experimental component. On the other hand, strong papers reproducing and comparing existing results experimentally do not require new theoretical insights. We encourage authors to provide any supplementary material that is required to support the claims made in the paper, such as detailed proofs or experimental data. These materials should be uploaded at submission time, as a single pdf or a tarball, not via a URL. It will be made available to reviewers only after they have submitted their first-draft reviews and hence need not be anonymized. Reviewers are under no obligation to look at the supplementary material but may refer to it if they have questions about the material in the body of the paper. Tool Papers Tool Papers should not exceed 6 pages, not counting references. These 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. Note that tool papers require the submission of an artifact for evaluation by the submission deadline. Artifacts will be evaluated concurrently with the review process and the program committee will have access to the artifact evaluation while making their decision. In special cases, where an artifact cannot be submitted, the authors should contact the program chairs to find alternate modes of artifact evaluation. Lightweight Double-Blind Reviewing Process CAV 2017 will employ a lightweight double-blind reviewing process. This means that committee members will not have access to authors=E2=80=99 names= or affiliations as they review a paper; however, authors=E2=80=99 names will be revealed once reviews have been submitted. To facilitate this, submitted papers must adhere to two rules: Author names and institutions must be omitted, and references to authors=E2= =80=99 own related work should be in the third person (e.g., not =E2=80=9CWe build= on our previous work=E2=80=A6=E2=80=9D but rather =E2=80=9CWe build on the work of= =E2=80=A6=E2=80=9D). The purpose of this process is to help the PC and external reviewers come to an initial judgement about the paper without bias, not to make it impossible for them to discover the authors if they were to try. Nothing should be done in the name of anonymity that weakens the submission, makes the job of reviewing the paper more difficult, or interferes with the process of disseminating new ideas. For example, important background references should *not* be omitted or anonymized, even if they are written by the same authors and share common ideas, techniques, or infrastructure. Authors should feel free to disseminate their ideas or draft versions of their paper as they normally would. For instance, authors may post drafts of their papers on the web or give talks on their research ideas. Artifact Submission and Evaluation Authors of accepted regular papers will be invited to submit (but are not required to submit) the relevant artifact for evaluation by the artifact evaluation committee. Authors of all tool papers are required to submit their artifact to the artifact evaluation committee at the paper submission time. Unlike regular papers, the results of the artifact evaluation for tool papers will be available to the program committee during the online discussions. To submit an artifact, please prepare a virtual machine (VM) image of your artifact and keep it accessible through an HTTP link throughout the evaluation process. As the basis of the VM image, please choose commonly used OS versions that have been tested with the virtual machine software and that evaluators are likely to be accustomed to. We encourage you to use https://www.virtualbox.org and save the VM image as an Open Virtual Appliance (OVA) file. Please include the prepared link in the appropriate field of the paper submission form. In addition, please supply at submission time a link to a short plain-text file describing the OS and parameters of the image, as well as the host platform on which you prepared and tested your virtual machine image (OS, RAM, number of cores, CPU frequency). Please describe how to proceed after booting the image, including the instructions for locating the full documentation for evaluating the artifact. If you are not in a position to prepare the artifact as above, please contact PC chairs for an alternative arrangement. It is to the advantage of authors to prepare an artifact that is easy to evaluate by the artifact evaluation committee and that yields expected results. We next provide some guidelines. Document in detail how to reproduce most of the experimental results of the paper using the artifact; keep this process simple through easy-to-use scripts and provide detailed documentation assuming minimum expertise of users. Ensure the artifact is in the state ready to run. It should work without a network connection. It should not require the user to install additional software before running. It should use reasonably modest resources (RAM, number of cores), so that the results can be reproduced on various hardware platforms including laptops. The evaluation should take reasonable amount of time to complete. When possible include source code within your virtual machine image and point to the most relevant and interesting parts of the source code tree. Members of the artifact evaluation committee and the program committee are asked to use submitted artifact for the sole purpose of evaluating the contribution associated with the artifact. Invited speakers * Chris Hawblitzel, Microsoft Research:Chris Hawblitzel, Microsoft Research Fast verification of fast cryptography for secure sockets * Marta Kwiatkowska, OxfordMarta Kwiatkowska, Oxford * Viktor Vafeiadis, MPI-SWSViktor Vafeiadis, MPI-SWS Formal reasoning under weak memory consistency Organization Conference co-chairs Viktor Kuncak, EPFL, Switzerland Rupak Majumdar, Max Planck Institute for Software Systems, Germany Workshop Chair Eva Darulov=C3=A1, Max Planck Institute for Software Systems, Germany Sponsorship Chair Barbara Jobstmann, EPFL and Cadence CAV Fellowship Chair Thomas Wahl, Northeastern University Publicity Chair Mika=C3=ABl Mayer, EPFL CAV Award Committee Tom Ball (Chair), Microsoft research Kim G. Larsen, Aalborg University Natarajan Shankar, SRI International Pierre Wolper, Liege University Program Committee Aws Albarghouthi Christel Baier Per Bjesse Jasmin Blanchette Sergiy Bogomolov Ahmed Bouajjani Rohit Chadha Bor-Yuh Evan Chang Swarat Chaudhuri Wei-Ngan Chin Hana Chockler Alessandro Cimatti Isil Dilig Dino Distefano Cezara Dragoi Michael Emmi Javier Esparza Georgios Fainekos Azadeh Farzan Aarti Gupta Gerard Holzmann Marieke Huisman Radu Iosif Franjo Ivancic Stefan Kiefer Zachary Kincaid Barbara K=C3=B6nig Daniel Kr=C3=B6ning Viktor Kuncak(Co-chair) Rustan Leino Rupak Majumdar (Co-chair) Kenneth McMillan Alexander Nadel Madhusudan Parthasarathy Corina Pasareanu Nadia Polikarpova Pavithra Prabhakar Arjun Radhakrishna Zvonimir Rakamaric Andrey Rybalchenko Roopsha Samanta Rahul Sharma Anna Slobodova Ana Sokolova Fabio Somenzi Zhendong Su Serdar Tasiran Emina Torlak Willem Visser Mahesh Viswanathan Yakir Vizel Tomas Vojnar Thomas Wahl Bow-Yaw Wang Georg Weissenbacher Verena Wolf Lenore Zuck Damien Zufferey Steering Committee Orna Grumberg, Technion, Israel Aarti Gupta, Princeton University, USA Daniel Kroening, University of Oxford, UK Kenneth McMillan, Microsoft Research, USA Artifact Evaluation Committee Ayca Balkan, UCLA Stephanie Balzer, CMU James Bornholt, University of Washington Simon Cruanes, INRIA Nancy Matthias Dangl University of Passau Marko Doko, MPI-SWS Chuchu Fan, UIUC Pietro Ferrara, Julia Johannes Hoelzl, TU Munich Lars Hupel, TU Munich Swen Jacobs, Saarland University Moa Johansson, Chalmers Dejan Jovanovic, SRI Ralf Jung, MPI-SWS Ivan Kuraj, MIT Andreas Lochbihler, ETH Zurich Jose Morales, IMDEA Van Chan Ngo, CMU Zvonimir Pavlinovic, NYU Markus Rabe, UC Berkeley Mukund Raghothaman, UPenn Andrew Reynolds, University of Iowa Nima Roohi, UIUC Christian Schilling, University of Freiburg Muralidaran Vijayaraghavan, MIT Nicolas Voirol, EPFL cavconference.org/2017 --94eb2c0895b4c9ceab05465dab21 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
CAV 2017: 29th International Conference = on Computer-Aided Verification
=


Important Dates: All deadlines are AOE (= Anywhere on Earth).

Papers:
=C2=A0 Paper= submission:= January 24, 2017 (Tuesday)
=C2=A0 Author response period= : Mar= ch 20-22, 2017 (Monday =E2=80=93 Wednesday)
=C2=A0 Author notific= ation: April 12, 2017 (Wednesday)
=C2=A0 Final version: May 5, 2017 (Fr= iday)

Conference:
=C2=A0 Workshops: July 22-= 23, 2017
=C2=A0 Main conference: July 24-28, 2017

=
Submission URL


S= cope

CAV 2017 is the 29th in a series dedicated to= the advancement of the theory and practice of computer-aided formal analys= is and synthesis methods for hardware and software systems.=C2=A0 CAV consi= ders it vital to continue spurring advances in hardware and software verifi= cation while expanding to domains such as cyber-physical, social, and biolo= gical systems.=C2=A0 The conference covers the spectrum from theoretical re= sults to concrete applications, with an emphasis on practical verification = tools and the algorithms and techniques that are needed for their implement= ation. The proceedings of the conference will be published in the Springer = LNCS series. A selection of papers will be invited to a special issue of Fo= rmal 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
Algorithms and tools for system synthesis
Mathematical and = logical foundations of verification and synthesis
Specifications = and correctness criteria for programs and systems
Deductive verif= ication using proof assistants
Hardware verification techniques
Program analysis and software verification
Software synt= hesis
Hybrid systems and embedded systems verification
= Compositional and abstraction-based techniques for verification
P= robabilistic and statistical approaches to verification
Verificat= ion methods for parallel and concurrent systems
Testing and run-t= ime analysis based on verification technology
Decision procedures= and solvers for verification and synthesis
Applications and case= studies in verification and synthesis
Verification in industrial= practice
New application areas for algorithmic verification and = synthesis
Formal models and methods for security
Formal= models and methods for biological systems


Paper Submission

NEW this year:
= There is no separate registration deadline. Full papers should be uploaded = by the submission deadline.
Tool papers require a concurrent arti= fact submission together with the paper submission. Artifact evaluation occ= urs concurrently with the review process and the PC gets access to the arti= fact evaluation during the PC discussions.
Submissions on a wide = range of topics are sought, particularly ones that identify new research di= rections.=C2=A0 CAV 2017 is not limited to topics discussed in previous ins= tances of the conference.=C2=A0 Authors concerned about the appropriateness= of a topic may communicate with the conference chairs prior to submission.=

As explained below, CAV 2017 will follow a lightw= eight double-blind review process.=C2=A0 Submissions that are not =E2=80=9C= blinded=E2=80=9D will be rejected without review.=C2=A0 Simultaneous submis= sion to other conferences with proceedings or submission of material that h= as already been published elsewhere is not allowed.=C2=A0 The review proces= s will include a feedback/rebuttal period where authors will have the optio= n to respond to reviewer comments.=C2=A0 The PC chairs may solicit further = reviews after the rebuttal period.

Papers must be = submitted in PDF format here

Submissions = will be in two categories: Regular Papers and Tool Papers.

Regular Papers

Regular Papers should not = exceed 16 pages in LNCS format, not counting references and appendices.=C2= =A0 Authors can include a clearly marked appendix at the end of their submi= ssions, that is exempt from the page limit restrictions. However, the revie= wers are not obliged to read the contents of these appendices.=C2=A0 These = papers should contain original research and sufficient detail to assess the= merits and relevance of the contribution.=C2=A0 Papers will be evaluated o= n basis of a combination of correctness, technical depth, significance, nov= elty, clarity, and elegance. We welcome papers on theory, case studies, and= comparisons with existing experimental research, as well as combinations o= f new theory with experimental evaluation.=C2=A0 A strong theoretical paper= is not required to have an experimental component.=C2=A0 On the other hand= , strong papers reproducing and comparing existing results experimentally d= o not require new theoretical insights.

We encoura= ge authors to provide any supplementary material that is required to suppor= t the claims made in the paper, such as detailed proofs or experimental dat= a.=C2=A0 These materials should be uploaded at submission time, as a single= pdf or a tarball, not via a URL.=C2=A0 It will be made available to review= ers only after they have submitted their first-draft reviews and hence need= not be anonymized.=C2=A0 Reviewers are under no obligation to look at the = supplementary material but may refer to it if they have questions about the= material in the body of the paper.

Tool Papers

Tool Papers should not exceed 6 pages, not counting = references.=C2=A0 These papers should describe system and implementation as= pects of a tool with a large (potential) user base (experiments not require= d, rehash of theory strongly discouraged).=C2=A0 Papers describing tools th= at have already been presented (in any conference) will be accepted only if= significant and clear enhancements to the tool are reported and implemente= d.=C2=A0 Note that tool papers require the submission of an artifact for ev= aluation by the submission deadline.=C2=A0 Artifacts will be evaluated conc= urrently with the review process and the program committee will have access= to the artifact evaluation while making their decision.=C2=A0 In special c= ases, where an artifact cannot be submitted, the authors should contact the= program chairs to find alternate modes of artifact evaluation.
<= br>
Lightweight Double-Blind Reviewing Process
CAV 2017= will employ a lightweight double-blind reviewing process. This means that = committee members will not have access to authors=E2=80=99 names or affilia= tions as they review a paper; however, authors=E2=80=99 names will be revea= led once reviews have been submitted.

To facilitat= e this, submitted papers must adhere to two rules:
Author names a= nd institutions must be omitted, and references to authors=E2=80=99 own rel= ated work should be in the third person (e.g., not =E2=80=9CWe build on our= previous work=E2=80=A6=E2=80=9D but rather =E2=80=9CWe build on the work o= f =E2=80=A6=E2=80=9D).

The purpose of this process= is to help the PC and external reviewers come to an initial judgement abou= t the paper without bias, not to make it impossible for them to discover th= e authors if they were to try.=C2=A0 Nothing should be done in the name of = anonymity that weakens the submission, makes the job of reviewing the paper= more difficult, or interferes with the process of disseminating new ideas.= For example, important background references should *not* be omitted or an= onymized, even if they are written by the same authors and share common ide= as, techniques, or infrastructure.=C2=A0 Authors should feel free to dissem= inate their ideas or draft versions of their paper as they normally would.= =C2=A0 For instance, authors may post drafts of their papers on the web or = give talks on their research ideas.



Artifact Submission and Evaluation

Authors of accepted regular papers will be invited to submit (but are not = required to submit) the relevant artifact for evaluation by the artifact ev= aluation committee.

Authors of all tool papers are= required to submit their artifact to the artifact evaluation committee at = the paper submission time. Unlike regular papers, the results of the artifa= ct evaluation for tool papers will be available to the program committee du= ring the online discussions.

To submit an artifact= , please prepare a virtual machine (VM) image of your artifact and keep it = accessible through an HTTP link throughout the evaluation process. As the b= asis of the VM image, please choose commonly used OS versions that have bee= n tested with the virtual machine software and that evaluators are likely t= o be accustomed to. We encourage you to use https://www.virtualbox.org and save the VM image as an Open Vir= tual Appliance (OVA) file. Please include the prepared link in the appropri= ate field of the paper submission form.

In additio= n, please supply at submission time a link to a short plain-text file descr= ibing the OS and parameters of the image, as well as the host platform on w= hich you prepared and tested your virtual machine image (OS, RAM, number of= cores, CPU frequency). Please describe how to proceed after booting the im= age, including the instructions for locating the full documentation for eva= luating the artifact.

If you are not in a position= to prepare the artifact as above, please contact PC chairs for an alternat= ive arrangement.

It is to the advantage of authors= to prepare an artifact that is easy to evaluate by the artifact evaluation= committee and that yields expected results. We next provide some guideline= s.=C2=A0 Document in detail how to reproduce most of the experimental resul= ts of the paper using the artifact; keep this process simple through easy-t= o-use scripts and provide detailed documentation assuming minimum expertise= of users. Ensure the artifact is in the state ready to run. It should work= without a network connection. It should not require the user to install ad= ditional software before running. It should use reasonably modest resources= (RAM, number of cores), so that the results can be reproduced on various h= ardware platforms including laptops. The evaluation should take reasonable = amount of time to complete. When possible include source code within your v= irtual machine image and point to the most relevant and interesting parts o= f the source code tree.

Members of the artifact ev= aluation committee and the program committee are asked to use submitted art= ifact for the sole purpose of evaluating the contribution associated with t= he artifact.


Invited speakers
=

* Chris Hawblitzel, Microsoft Research:Chris Hawblitzel= , Microsoft Research
=C2=A0 Fast verification of fast cryptograph= y for secure sockets

* Marta Kwiatkowska, OxfordMa= rta Kwiatkowska, Oxford

* Viktor Vafeiadis, MPI-SW= SViktor Vafeiadis, MPI-SWS
=C2=A0 Formal reasoning under weak mem= ory consistency


Organization
<= div>
Conference co-chairs
Viktor Kuncak, EPFL, Swit= zerland
Rupak Majumdar, Max Planck Institute for Software Systems= , Germany

Workshop Chair
Eva Darulov=C3= =A1, Max Planck Institute for Software Systems, Germany

Sponsorship Chair
Barbara Jobstmann, EPFL and Cadence
=

CAV Fellowship Chair
Thomas Wahl, Northeaster= n University

Publicity Chair
Mika=C3=ABl= Mayer, EPFL

CAV Award Committee
Tom Bal= l =C2=A0(Chair), Microsoft research
Kim G. Larsen, Aalborg Univer= sity
Natarajan Shankar, SRI International
Pierre Wolper= , Liege University

Program Committee
Aws= Albarghouthi
Christel Baier
Per Bjesse
Jasmi= n Blanchette
Sergiy Bogomolov
Ahmed Bouajjani
Rohit Chadha
Bor-Yuh Evan Chang
Swarat Chaudhuri
=
Wei-Ngan Chin
Hana Chockler
Alessandro Cimatti
Isil Dilig
Dino Distefano
Cezara Dragoi
Michael Emmi
Javier Esparza
Georgios Fainekos
Azadeh Farzan
Aarti Gupta
Gerard Holzmann
= Marieke Huisman
Radu Iosif
Franjo Ivancic
Ste= fan Kiefer
Zachary Kincaid
Barbara K=C3=B6nig
Daniel Kr=C3=B6ning
Viktor Kuncak(Co-chair)
Rustan Lei= no
Rupak Majumdar (Co-chair)
Kenneth McMillan
Alexander Nadel
Madhusudan Parthasarathy
Corina Pasare= anu
Nadia Polikarpova
Pavithra Prabhakar
Arju= n Radhakrishna
Zvonimir Rakamaric
Andrey Rybalchenko
Roopsha Samanta
Rahul Sharma
Anna Slobodova
Ana Sokolova
Fabio Somenzi
Zhendong Su
Serdar Tasiran
Emina Torlak
Willem Visser
Ma= hesh Viswanathan
Yakir Vizel
Tomas Vojnar
Tho= mas Wahl
Bow-Yaw Wang
Georg Weissenbacher
Ver= ena Wolf
Lenore Zuck
Damien Zufferey

Steering Committee
Orna Grumberg, Technion, Israel
Aarti Gupta, Princeton University, USA
Daniel Kroening, Univer= sity of Oxford, UK
Kenneth McMillan, Microsoft Research, USA

Artifact Evaluation Committee
Ayca Balkan, U= CLA
Stephanie Balzer, CMU
James Bornholt, University of= Washington
Simon Cruanes, INRIA Nancy
Matthias Dangl U= niversity of Passau
Marko Doko, MPI-SWS
Chuchu Fan, UIU= C
Pietro Ferrara, Julia
Johannes Hoelzl, TU Munich
Lars Hupel, TU Munich
Swen Jacobs, Saarland University
Moa Johansson, Chalmers
Dejan Jovanovic, SRI
Ralf= Jung, MPI-SWS
Ivan Kuraj, MIT
Andreas Lochbihler, ETH = Zurich
Jose Morales, IMDEA
Van Chan Ngo, CMU
= Zvonimir Pavlinovic, NYU
Markus Rabe, UC Berkeley
Mukun= d Raghothaman, UPenn
Andrew Reynolds, University of Iowa
Nima Roohi, UIUC
Christian Schilling, University of Freiburg
Muralidaran Vijayaraghavan, MIT
Nicolas Voirol, EPFL

--94eb2c0895b4c9ceab05465dab21--