From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: 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 7CBDE7FEFC for ; Thu, 17 Jan 2019 09:27:32 +0100 (CET) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=c.a.furia@gmail.com; spf=Pass smtp.mailfrom=c.a.furia@gmail.com; spf=None smtp.helo=postmaster@mail-ed1-f54.google.com Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of c.a.furia@gmail.com) identity=pra; client-ip=209.85.208.54; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="c.a.furia@gmail.com"; x-sender="c.a.furia@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of c.a.furia@gmail.com designates 209.85.208.54 as permitted sender) identity=mailfrom; client-ip=209.85.208.54; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="c.a.furia@gmail.com"; x-sender="c.a.furia@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-ed1-f54.google.com) identity=helo; client-ip=209.85.208.54; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="c.a.furia@gmail.com"; x-sender="postmaster@mail-ed1-f54.google.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3AduD92hAOvrotrOE/xxsLUyQJP3N1i/DPJgcQr6Af?= =?us-ascii?q?oPdwSPvzocbcNUDSrc9gkEXOFd2Cra4c26yO6+jJYi8p2d65qncMcZhBBVcuqP?= =?us-ascii?q?49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6?= =?us-ascii?q?JvjvGo7Vks+7y/2+94fcbglUhzexe69+IAmrpgjNq8cahpdvJLwswRXTuHtIfO?= =?us-ascii?q?pWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+VrxYES8pM3sp683xtBnM?= =?us-ascii?q?VhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs5Xymp4aV2Rx/ykC?= =?us-ascii?q?oJND43/m/JhMxqkaxWuw6tqwBlzoLIfI2ZKOZyc6XAdt0aX2pBWcNRWjRODYyi?= =?us-ascii?q?dYsPDuQBPOZGoYn9plsOtga1CA6wC+/10DBEnHH23bAg0+QgCw7LxwMgH9cUv3?= =?us-ascii?q?TVqNX5LrsdUeewzKTRyzjIcv1Y2TD46IfScxAhp+mBUqxsccrRyEgjDR/KjlWW?= =?us-ascii?q?pIf4PD2VzvwAv3aH4+dkT+6iiG4qpxtvrjSzxcogkInEi40NxlzZ8Sh0wJw5Kc?= =?us-ascii?q?C6RUN6e9KoDZlduiKAO4drQc4vQmdlszsgxLIco560Zi0KxYwnxxHBb/yHdJCF?= =?us-ascii?q?4hf5W+aQJTd0nWxqd6+iixqr/0ityuLxWtO70FZNqSpFnd3MuW4X2xPP7ciHT+?= =?us-ascii?q?Nx/kan2TmRywDe8v9ILVwwmKbBKJMswqQ8moQPvUnABCP7mEr7gLeTdko+++io?= =?us-ascii?q?7+rnYq/hpp+ZL4J7lhvyPb40lsyxHOQ4KAkOUHKA9OSz0b3s50z5QLFQgvIqla?= =?us-ascii?q?nZtYjWJd4Hqa6hHw9VzoEj5g6jADi81dQYmWALLFZEeBKck4jkIErOIfD9Dfen?= =?us-ascii?q?mVugijZrx/bcPr3gGJrBNHbDkK2yNYp6vkVVzQ52ydFE+7pVDKsAKbT9QBzLuc?= =?us-ascii?q?TcHyM+ZjK52efpGel915hWDXyCGK6XIb/SsESg7flpJfSNYckUtWCuBeIi4qvQ?= =?us-ascii?q?gGU4l04hfaiylc8cLnn+EOl8Ikyxbn/lg9NHGmAP6FltBNf2gUGPBGYAL025WL?= =?us-ascii?q?gxs2liWdCWSLzbT4Xou4SvmSKyH5lYfGdDUwneHnLhdoHCUPAJOnvLfp1R1wcc?= =?us-ascii?q?XL3kcLcPkAm0vVajmbViJ+vQvCYfsMC7jYUn16jojRg3sAdMIYGd3mWKFTwmm2?= =?us-ascii?q?oJQ3o70Pk6rxEhjFiE1qd8jrpTEtkBv/4=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0AqAwB2O0BchzbQVdFjBoIRgVuBD4Epj?= =?us-ascii?q?HqLA1ABB4QdhzoBjVsUgWcLAQEFGg2BS4M4ghMaBwEEMAkNAQMBAQIBAQEBARM?= =?us-ascii?q?BAQEIDQkIKSMMgjoigxICIQEbDBIDEmkFEQEFATUbgjxLAYFoAQMIDQSfBzyDU?= =?us-ascii?q?ohbBQEXgngFhEIKGScNXoE3AgYJAQiMLXoVgQeDboF2gw0BEgGDVYIqAqFpJwc?= =?us-ascii?q?CgWCBPoQEiwmCModch32aZwYCCQcPIThtgR1xcIM8CYIqAoMsKIpUPjOBAiYTh?= =?us-ascii?q?zqCPgEB?= X-IPAS-Result: =?us-ascii?q?A0AqAwB2O0BchzbQVdFjBoIRgVuBD4EpjHqLA1ABB4Qdhzo?= =?us-ascii?q?BjVsUgWcLAQEFGg2BS4M4ghMaBwEEMAkNAQMBAQIBAQEBARMBAQEIDQkIKSMMg?= =?us-ascii?q?joigxICIQEbDBIDEmkFEQEFATUbgjxLAYFoAQMIDQSfBzyDUohbBQEXgngFhEI?= =?us-ascii?q?KGScNXoE3AgYJAQiMLXoVgQeDboF2gw0BEgGDVYIqAqFpJwcCgWCBPoQEiwmCM?= =?us-ascii?q?odch32aZwYCCQcPIThtgR1xcIM8CYIqAoMsKIpUPjOBAiYThzqCPgEB?= X-IronPort-AV: E=Sophos;i="5.56,488,1539640800"; d="scan'208";a="292220440" Received: from mail-ed1-f54.google.com ([209.85.208.54]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 17 Jan 2019 09:27:31 +0100 Received: by mail-ed1-f54.google.com with SMTP id h50so7648067ede.5 for ; Thu, 17 Jan 2019 00:27:31 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=message-id:from:date:to:reply-to:cc:subject; bh=kqA7n4q+C84q2lUPlUY0vwQ3RXocGW9CCAHXgnlk+Ys=; b=VnBHhLpUbgmWslZgVy/pDR4l9o2rP1of9Aa3v6luzyww3FaiPgyM1OkP/MIETUUi39 z4kESBb/Ih4pMvyjwn3R1XIk3luWFbHuHGuLqR9SE65s3vAyHNWY7xFJ3u6iIJe1i+ZN fDCJrftYvIyDv0mAaJ6ZHVkHvsVkNEoF4GzK1f0gUpRM8Bs9q50Qxp2ic9r0D/lhZSmP naLD4yH0u0qJEBrqwVrydfdbSY+/IZQltC2Px0bAjaXGmhq8i0N9g9PRnMPdGrLNksIq QQusIUNGmoEJ+bemSYu00vq3NEoxX007IkbeHor75pn7Ex8ERs1CQM1jG7sF064CWfHG AlJg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:message-id:from:date:to:reply-to:cc:subject; bh=kqA7n4q+C84q2lUPlUY0vwQ3RXocGW9CCAHXgnlk+Ys=; b=C7DANqtCw77KFhjFHfQC6ZXR+AlnyUavvZxNmgP6Pm+NpLuVjADDDunTBD3n1NVLhO QigsLRUbF3pUZGEr5aDjk9g3lShOPCzWQX00ZixhL8WT963c1iTiD2rprx8Ye/ka5pWH 6p6QOqHWHiv4miWev73KDWcnPLZXu6lHPr3T7MjFwhtQG8bRh4xTfF4IfAHDjiLSaphC CEcOceigniXnCNvwuIXbktRFsXIS40I9FYdS2HZUEg4aZeBl+LJ7P5Kx1wt0KSNrGd3h tFk/d1ZLg66B+t377jOVIPTAg1ynBzZbR3pODhCiRACi9bJjsyDQ5IOWhs6Aqp1HHgiD 3Skw== X-Gm-Message-State: AJcUukeSLZ/9S3j4vSpaw4ShmZHtTa+mJkVKe/977hsVd8GdzpdnXAt7 IWQz2KwZ8J3MPvO2PNBzmE1MAlFQJ3bkKw== X-Google-Smtp-Source: ALg8bN4SXvfM6BNOh8Ka0viKDVN9yxw6r1WSW9IEr66YZ+BChhFa7kh542AomFW+q4Eu/NMCHUfxkQ== X-Received: by 2002:a50:a5b8:: with SMTP id a53mr11049708edc.199.1547713650583; Thu, 17 Jan 2019 00:27:30 -0800 (PST) Received: from localhost (nat186.lu.usi.ch. [195.176.178.186]) by smtp.gmail.com with ESMTPSA id a11sm6690213edc.28.2019.01.17.00.27.29 for (version=TLS1_2 cipher=ECDHE-RSA-CHACHA20-POLY1305 bits=256/256); Thu, 17 Jan 2019 00:27:29 -0800 (PST) Message-ID: <5c403c71.1c69fb81.eb2cf.a6b0@mx.google.com> From: VerifyThis X-Google-Original-From: VerifyThis Date: Thu, 17 Jan 2019 09:27:29 +0100 To: caml-list@inria.fr Reply-To:VerifyThis Cc: X-Validation-by: c.a.furia@gmail.com Subject: [Caml-list] VerifyThis at ETAPS 2019: 2nd Call for Problems ******************************************************************************* VerifyThis Verification Competition 2019 ACCOUNCEMENT AND CALL FOR PROBLEMS Competition to be held at ETAPS 2019 http://verifythis.ethz.ch ******************************************************************************** Get involved, even if you cannot participate in the competition: provide a challenge! IMPORTANT DATES Problems submission deadline: 28 January 2019 Competition: 6 and 7 April 2019 ABOUT THE COMPETITION VerifyThis 2019 will take place as part of the European Joint Conferences on Theory and Practice of Software (ETAPS 2019) on 6 and 7 April 2019. It is the 8th event in the VerifyThis competition series. Information on previous events and participants can be found at http://verifythis.ethz.ch The aims of the competition are: - to bring together those interested in formal verification, and to provide an engaging, hands-on, and fun opportunity for discussion - to evaluate the usability of logic-based program verification tools in a controlled experiment that could be easily repeated by others. The competition will offer a number of challenges presented in natural language. Participants have to formalize the requirements, implement a solution, and formally verify the implementation for adherence to the specification. There are no restrictions on the programming language and verification technology used. The correctness properties posed in problems will have the input-output behaviour of programs in focus. Solutions will be judged for correctness, completeness and elegance. CALL FOR PROBLEMS To be able to offer a broad and diverse set of verification challenges, we are collecting submissions of ideas for verification challenges and problems. We welcome both problems of academic interest as well as challenges based on themes that are relevant in industry. We encourage suggestions at any level of detail, including submissions without a fully worked out verification task. - a problem may contain an informal statement of the algorithm to be implemented (optionally with complete or partial pseudocode) and the requirement(s) to be verified - a problem should be solvable, at least in part, within a 60-90 minute time slot - submission of reference solutions is welcome but not mandatory - problems mainly suitable for specific languages or tools should be clearly identified as such - problems that contain several subproblems or other means of difficulty scaling are especially welcome - the organizers reserve the right (but no obligation) to use the problems in the competition, either as submitted or with modifications - submissions from (potential) competition participants are allowed Problems from previous competitions can be seen at http://verifythis.ethz.ch Submissions are to be sent by email to verifythis@cs.nuim.ie by the date indicated above. PRIZES The submission most interesting and suitable for the competition will receive a prize. ORGANIZERS * Claire Dross, AdaCore, France * Carlo A. Furia, Università della Svizzera Italiana (USI), Switzerland * Marieke Huisman, University of Twente, the Netherlands * Rosemary Monahan, Maynooth University, Ireland * Peter Müller, ETH Zürich, Switzerland CONTACT Email: verifythis@cs.nuim.ie Web: http://verifythis.ethz.ch