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 CDD567FD2F for ; Sat, 4 Mar 2017 23:31:01 +0100 (CET) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=compscience.announcement@gmail.com; spf=Pass smtp.mailfrom=compscience.announcement@gmail.com; spf=None smtp.helo=postmaster@mail-vk0-f66.google.com Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of compscience.announcement@gmail.com) identity=pra; client-ip=209.85.213.66; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="compscience.announcement@gmail.com"; x-sender="compscience.announcement@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of compscience.announcement@gmail.com designates 209.85.213.66 as permitted sender) identity=mailfrom; client-ip=209.85.213.66; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="compscience.announcement@gmail.com"; x-sender="compscience.announcement@gmail.com"; 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@mail-vk0-f66.google.com) identity=helo; client-ip=209.85.213.66; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="compscience.announcement@gmail.com"; x-sender="postmaster@mail-vk0-f66.google.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3Ati5gSRHgyJaky/PcpJtf8J1GYnF86YWxBRYc798d?= =?us-ascii?q?s5kLTJ7zrs2wAkXT6L1XgUPTWs2DsrQf2reQ6P+rATVIyK3CmUhKSIZLWR4BhJ?= =?us-ascii?q?detC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+?= =?us-ascii?q?KPjrFY7OlcS30P2594HObwlSijewZbN/IA+4oAjTucUanZZuIbstxxXUpXdFZ/?= =?us-ascii?q?5Yzn5yK1KJmBb86Maw/Jp9/ClVpvks6c1OX7jkcqohVbBXAygoPG4z5M3wqBnM?= =?us-ascii?q?VhCP6WcGUmUXiRVHHQ7I5wznU5jrsyv6su192DSGPcDzULs5Vyiu47ttRRT1jy?= =?us-ascii?q?gKKzA0/H3KhsBpkK5XvQ+qqxhiz4PUZY2YMud1cKHActMAXWdPXshfWS9cDI2i?= =?us-ascii?q?c4QCEvEMMvxEo4TnvVYCsQeyCAuqCejyyjFInHj23agi3uokFQHJxhEgH8kTu3?= =?us-ascii?q?rWttr1KrkdUeSozKnO0DrIcvRb1iv66IjNahAhuu2DXbNufsrX1UYgCRnJgU+W?= =?us-ascii?q?qYzjODOVy+INvHSF4OplS+2vjXInphp+ojiq3Mgsi43JipgJxVDD8CV02YA4Ls?= =?us-ascii?q?C2Rk58ZN6rCppQtyeCOotsXMwiWXpotD8mxb0Go5G7eCwKx4ohxx7QdfOLaY+I?= =?us-ascii?q?4gjsVOuXPDx2h2pldaqhixqu9UWs0O7xW8mu3FpUsyZInMPAu3EM2hHV98OJUO?= =?us-ascii?q?Fy/l271jaKzw3T6v9LIUQzlafDLp4u2L8wlp4KvUTdHS/6hFz6jKGXe0gl4OSo?= =?us-ascii?q?5OPnYrLppp+YKYB4kB3xMqMrmsCnAOQ4NBYBX3SD9OiiyLHu+Vf1TbZKg/EsjK?= =?us-ascii?q?XVrZ7XKd4aq6O4GwNV15ws6xe7DzeoytQYmnwHIUpZdxKAiojpI0rOL+z5Dfih?= =?us-ascii?q?hVSjjClky+rcMb3nBJXNKWXDkLH9crlj7k5T1gwzzcxE6pJbD7EOOvPzWkvruN?= =?us-ascii?q?PECR85NhS4w/z7B9VlyoMeRWWPD7eFP6zItF+I4vsjI+2NZI8OpDbwMOMl5v7r?= =?us-ascii?q?jX8hg1ARZ6ip3Z0NaHC5BPtqOUuZYWC/yusGREQOtxclBMzjllCGTDhfLyK5WK?= =?us-ascii?q?ck/To6BYStAMHKQIaqnbqK0SK2GIF+aWVPC1TKGnDtIdaqQfAJPQGWK9J62hwN?= =?us-ascii?q?S7WlVoktnUWlswri0LFmI+zf92sRs5Tkyd5+6ujekw0a+jl9DsDb2GaIGTIn1l?= =?us-ascii?q?gUTiM7ifgs6Xd2zU2OhPEljg=3D=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0DsBADEP7tYbELVVdFEFAaDHjkqIgEzC?= =?us-ascii?q?3gSB4NYq12DHYQcAiiCQoYXB0MUAQEBAQEBAQEBAQESCwsLBiovgjMKgwIdAQg?= =?us-ascii?q?THgMSEDcCJAERAQUBIicHAYlHAQMIDQ4xoWSDQz+KVwKBKoIEBQEcGYJwBYNNC?= =?us-ascii?q?hknDVWCcioCBhIgigKBCYMXgS+DFIJfBZBViwpNkjOBe4UiigACiSWITxQegRU?= =?us-ascii?q?2gSQ3H2uEBG+Bax81AYo5AQEB?= X-IPAS-Result: =?us-ascii?q?A0DsBADEP7tYbELVVdFEFAaDHjkqIgEzC3gSB4NYq12DHYQ?= =?us-ascii?q?cAiiCQoYXB0MUAQEBAQEBAQEBAQESCwsLBiovgjMKgwIdAQgTHgMSEDcCJAERA?= =?us-ascii?q?QUBIicHAYlHAQMIDQ4xoWSDQz+KVwKBKoIEBQEcGYJwBYNNChknDVWCcioCBhI?= =?us-ascii?q?gigKBCYMXgS+DFIJfBZBViwpNkjOBe4UiigACiSWITxQegRU2gSQ3H2uEBG+Ba?= =?us-ascii?q?x81AYo5AQEB?= X-IronPort-AV: E=Sophos;i="5.35,244,1484002800"; d="scan'208,217";a="215583005" Received: from mail-vk0-f66.google.com ([209.85.213.66]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 04 Mar 2017 23:30:42 +0100 Received: by mail-vk0-f66.google.com with SMTP id d188so860079vka.3 for ; Sat, 04 Mar 2017 14:30:42 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:from:date:message-id:subject:to; bh=VrwgLQhVVwSCtwRcsvhSpbjQwCL9R+SlzMT5uR/vAN8=; b=OURM01Mcvr/XBCuWndd+tAmSwQUABZEMgbmpdYtBcg/uEktWU1oevw3ysUcvc4vjYL ud9hcVzGPqA2Tc8isP6WYZYTeactA3SkrD1oE+bkEu7PuUwr0TTdCPjGRf0sYXOWnXVV zh0VmpmTrGPEo4/jfwMT6UEKhfg3hIdVaJzd+j87mImeemxV68MNN5Uy1Pwk/fRe4576 7pQ8oPZDuYM0JMMWOVkICgGP/B1gy3obnCklPU4KiOmFTF/TkmUoTukQ8p5pNuhk6iTR o3eqCx4Q585l0Ghcxfg3MPneihV9QhSMTLyiBrfsqjJQYLGHimoVODeKb9qkpZv/Xu91 uoDw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:mime-version:from:date:message-id:subject:to; bh=VrwgLQhVVwSCtwRcsvhSpbjQwCL9R+SlzMT5uR/vAN8=; b=IVubpuWT/BL0CfzJvC9FUwKISRA2PVNlplz8C/ulmqEHFRqdZUFFTGROvFzaLlSF+A bmw7eVCCPJIEH+/mebZX18QkvP2sYbPBFJOldl2vonjDKDKk7Al2JAkKsUPbMzaAQEzG Jg5nDOqK6KR3CnVSKdsXWQh6ZtQy5PU2oaAAkWsrAZ0DaYkt0wa9TvzwVIBaDuaw3Uhg qxkFDvv+H3VqQn6fPfhQCLt+qm5PZhddqLRH2Gks7eC7XCig9EHLX09RkXU1ijOxvvqW uNQkymkaAJl44lbFKw7nin7wMb/Ms5Xp43lzd6RQP1HN4yzMa/D4NQwRmwObbLvY9hsx OQjg== X-Gm-Message-State: AMke39lflNAtmCSxZKa5+VFVFFO/W80qv2PLhojJHQaZbRPR4zWuab5pibm+5J5G/6wesKC41dyJ4n32qlyGWg== X-Received: by 10.31.178.137 with SMTP id b131mr3843458vkf.70.1488666640861; Sat, 04 Mar 2017 14:30:40 -0800 (PST) MIME-Version: 1.0 Received: by 10.176.84.129 with HTTP; Sat, 4 Mar 2017 14:30:40 -0800 (PST) From: Klaus Havelund Date: Sat, 4 Mar 2017 14:30:40 -0800 Message-ID: To: Klaus Havelund Content-Type: multipart/alternative; boundary=001a11438b2c51555b0549ef360a Subject: [Caml-list] RERS: 7th International Challenge on the Rigorous Examination of Reactive Systems --001a11438b2c51555b0549ef360a Content-Type: text/plain; charset=UTF-8 Dear colleagues, The *RERS Challenge* *2017*: is the 7th International Challenge on the Rigorous Examination of Reactive Systems and is *co-located with ISSTA/SPIN 2017*. The event will be held in *July 2017, in Santa Barbara, USA*. RERS is designed to encourage software developers and researchers to apply and combine their tools and approaches in a free style manner to answer evaluation questions for reachability and LTL formulas on specifically designed benchmarks. The goal of this challenge is to provide a basis for the comparison of verification techniques and available tools. The benchmarks are automatically synthesized to exhibit chosen properties and then enhanced to include dedicated dimensions of difficulty, ranging from conceptual complexity of the properties (e.g. reachability, full safety, liveness), over size of the reactive systems (a few hundred lines to tens of thousands of them), to exploited language features (arrays and index arithmetics). They are therefore especially suited for community-overlapping tool comparisons. What distinguishes RERS from other challenges is that the challenge problems can be approached in a free-style manner: it is highly encouraged to combine and exploit all known (even unusual) approaches to software verification. In particular, participants are not constrained to their own tools. To clearly separate RERS from other challenges, this year the LTL analysis is separated from the reachability of labels. RERS is then the only challenge with a special track for LTL analysis on synthesized benchmarks. The main aims of RERS 2017 are to : * encourage the combination of usually different research fields for better software verification results * provide a comparison foundation based on differently tailored benchmarks that reveals the strengths and weaknesses of specific approaches * initiate a discussion for better benchmark generation reaching out across the usual community barriers to provide benchmarks useful for testing and comparing a wide variety of tools There will be a 1 day workshop where the results will be presented, the generation methodology will be explained, and the modalities for the RERS 2018 challenge, which will be part of ISoLA 2018 will be discussed. There is still a lot of time to get engaged, and collecting RERS achievements is a lot of fun! In addition there will be book prices sponsored by Springer. Schedule: ========= SEQUENTIAL PROBLEMS =================== The sequential challenge just started. Its entire setup in online since a few days. Thus you can start right away. At least if you are a RERS newcomer, we would strongly recommend you to start with the training problems: ( http://www.rers-challenge.org/2017/index.php?page=trainingphase) They are an ideal starting point for the challenge: They are smaller in size than the challenge problems but otherwise structurally equivalent. Moreover, an automatic checker (available on the same page) allows you to evaluate your own solutions. After having tackled the training problems it should be easy to move on to attack the challenge problems. PARALLEL PROBLEMS ================= 01.03.2017: The training problems for the parallel challenge wil be online 01.05.2017: The setup for the parallel challlenge will be online. *DEADLINE for all submission* =========================== *01.07.2017* Please note that we want to specifically encourage also solutions from participants that work with tools developed by others. More detailed information on the challenge can be found in the participants section of www.rers-challenge.org/2017. Looking forward to seeing you in Santa Barbara! Best regards Bernhard, Falk, Jaco, and Markus --001a11438b2c51555b0549ef360a Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable

Dear colleagues,=20 The RERS Challenge 2017: is the 7th International Challenge on the Rigorous Examination of Reactive Systems and is co-located with ISST= A/SPIN 2017. The event will be held in July 2017, in Santa Barbara, USA<= /font>. RERS is designed to encourage software developers and researchers to apply and combine their tools and approaches in a free style manner to answer evaluation questions for reachability and LTL formulas on specifically designed benchmarks. The goal of this challenge is to provide a basis for the comparison of verification techniques and available tools. The benchmarks are automatically synthesized to exhibit chosen properties and then enhanced to include dedicated dimensions of difficulty, ranging from conceptual complexity of the properties (e.g. reachability, full safety, liveness), over size of the reactive systems (a few hundred lines to tens of thousands of them), to exploited language features (arrays and index arithmetics). They are therefore especially suited for community-overlapping tool comparisons. What distinguishes RERS from other challenges is that the challenge problems can be approached in a free-style manner: it is highly encouraged to combine and exploit all known (even unusual) approaches to software verification. In particular, participants are not constrained to their own tools. To clearly separate RERS from other challenges, this year the LTL analysis is separated from the reachability of labels. RERS is then the only challenge with a special track for LTL analysis on synthesized benchmarks. The main aims of RERS 2017 are to : * encourage the combination of usually different research fields for better software verification results * provide a comparison foundation based on differently tailored benchmarks that reveals the strengths and weaknesses of specific approaches * initiate a discussion for better benchmark generation reaching out across the usual community barriers to provide benchmarks useful for testing and comparing a wide variety of tools There will be a 1 day workshop where the results will be presented, the=20 generation methodology will be explained, and the modalities for the RERS 2018 challenge, which will be part of ISoLA 2018 will be discussed. There is still a lot of time to get engaged, and collecting RERS achievements is a lot of fun! In addition there will be book prices sponsored by Springer.=20 Schedule: =3D=3D=3D=3D=3D=3D=3D=3D=3D SEQUENTIAL PROBLEMS =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D The sequential challenge just started. Its entire setup in online since a few days. Thus you can start right away. At least if you are a RERS newcomer, we would strongly recommend you to start with the training problems: (http= ://www.rers-challenge.org/2017/index.php?page=3Dtrainingphase= ) They are an ideal starting point for the challenge: They are smaller in size than the challenge problems but otherwise structurally equivalent. Moreover, an automatic checker (available on the same page) allows you to evaluate your own solutions. After having tackled the training problems it should be easy to move on to attack the challenge problems. PARALLEL PROBLEMS =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D 01.03.2017: The training problems for the parallel challenge wil be online= =20 01.05.2017: The setup for the parallel challlenge will be online. DEADLINE for all submission =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D 01.07.2017 =C2=A0 Please note that we want to specifically encourage also solutions from participants that work with tools developed by others. More detailed information on the challenge can be found in the participants section of www.rers-challenge.org/2017. Looking forward to seeing you in Santa Barbara! Best regards Bernhard, Falk, Jaco, and Markus
--001a11438b2c51555b0549ef360a--