From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by c5ff346549e7 (Postfix) with ESMTP id EF5AD5D5 for ; Mon, 9 Apr 2018 09:10:14 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.48,426,1517871600"; d="scan'208,217";a="321894459" Received: from sympa.inria.fr ([193.51.193.213]) by mail2-relais-roc.national.inria.fr with ESMTP; 09 Apr 2018 11:10:12 +0200 Received: by sympa.inria.fr (Postfix, from userid 20132) id D2C1A82446; Mon, 9 Apr 2018 11:10:12 +0200 (CEST) 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 30DA08240C for ; Mon, 9 Apr 2018 11:10:03 +0200 (CEST) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=david.baelde@gmail.com; spf=Pass smtp.mailfrom=david.baelde@gmail.com; spf=None smtp.helo=postmaster@mail-wr0-f170.google.com IronPort-PHdr: =?us-ascii?q?9a23=3AbTFTrB8h5zY+xf9uRHKM819IXTAuvvDOBiVQ1KB3?= =?us-ascii?q?0uMcTK2v8tzYMVDF4r011RmVBd6ds6oMotGVmpioYXYH75eFvSJKW713fDhBt/?= =?us-ascii?q?8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1?= =?us-ascii?q?Ifn+FpLPg8it2O2+55Pebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+?= =?us-ascii?q?RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTF?= =?us-ascii?q?UACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMNboRr4oRzut86ZrSAfpiC?= =?us-ascii?q?gZMT457HrXgdF0gK5CvR6tuwBzz4vSbYqINvRxY7ndcMsaS2RPXchfSjJPDZ+n?= =?us-ascii?q?YoQVE+YMJ/xVo5Xhq1YMqxa1GAmiBPnoyj9NnnL407c10/ogEQ7bwQctAsgBv2?= =?us-ascii?q?rQrNroKqgZTOe4w7TSwjXdbvNZxC3x55PSfR8/pfGDQKx/fNHeyUkqDQzFj1GQ?= =?us-ascii?q?pZb5MDOS0+QAqm6W5PduW+Kojm4osQBxoj63y8cokYnJmJgZyl7e9Sh/3Y07Js?= =?us-ascii?q?W4RVZlbdK4FJZcrSKXOotsTs8/XW1luzw2xqAEtJKneiUB1Y4pyATFa/OddoiF?= =?us-ascii?q?+hLjW/iVITd/nH9lfaiwhxe28US5xOz8TNW43E9EriZYkNTAqmoB1xPU6siARf?= =?us-ascii?q?t9+lmu1SyT2ADU7+FIOUE0lazFJJ492rM8iIYfvEDZEiL1mEj6lrKaelsn9+Sy?= =?us-ascii?q?9ujqYKnqqoeZN4BuiwH+Nqoumta4AeQ9KgUBQnKU+fq91LL+50H2W69FgeMykq?= =?us-ascii?q?bErp/XPssbpqujDA9U1oYv8QqwDzCj0NgAh3kIMEpFeA6bj4juI1zBPOr3DfK7?= =?us-ascii?q?g1i1lDdrxuvGPqH6D5XWLnnDla/hcqxn505dzgoz19Ff6IhOBrEPOvKgEnP24f?= =?us-ascii?q?vzBxo9eym9wuLmDto18oIFRSrbCaacNObWsESUzuMpOeiFIoEP7nK1K/E+5PPq?= =?us-ascii?q?iVc5kEQecK2tm5wNZyOWBPNjdmmQf3vgyv0IHGMGs0JqQOX0iVHEWzdeY3q/d6?= =?us-ascii?q?057zA/TomhCNGQFciWnLWd0XLjTdVtbWdcBwXJSC+wLtTWa7I3cCuXZ/RZvHkB?= =?us-ascii?q?XLmlRZUm0Ej35gD/wrtjaOHT/39B7M6x5J1O/+TW0CoK23lsFc3EijOCSmh1mi?= =?us-ascii?q?UDQDpkhPki83w48U+K1O1Du9IdFdFX4KkXAAIzNJqZ0PYiTt6rBVqHcdCOR1Kr?= =?us-ascii?q?BN6hBGNpQw=3D=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0ByAACQLctaf6qAVdFbg0iBDG8oCoMXP?= =?us-ascii?q?4EdQpMsgwOHSIsVgXoLBRqBW4FHgUKCNAcZBwEEMBgBAgEBAQEBAQEBARMBAQk?= =?us-ascii?q?LCwgmJQxCEAGBYiQBglsRBh0BGx4DEgMGBzcCJAERAQUBIgGFBgEDFYkXj388i?= =?us-ascii?q?wWBfwUBF4JvBYNIChkmDVRXghYCAQUSh1mBVD+BDIIaPIFvg1uCU4JUApdHCIF?= =?us-ascii?q?gg3aIX4Eygh+BPIc2hQCEHIZbDwMegQQcggozGiOBAIISgXA8gQUBAoJIgT6JF?= =?us-ascii?q?j0wiFSEMiuCGAEB?= X-IPAS-Result: =?us-ascii?q?A0ByAACQLctaf6qAVdFbg0iBDG8oCoMXP4EdQpMsgwOHSIs?= =?us-ascii?q?VgXoLBRqBW4FHgUKCNAcZBwEEMBgBAgEBAQEBAQEBARMBAQkLCwgmJQxCEAGBY?= =?us-ascii?q?iQBglsRBh0BGx4DEgMGBzcCJAERAQUBIgGFBgEDFYkXj388iwWBfwUBF4JvBYN?= =?us-ascii?q?IChkmDVRXghYCAQUSh1mBVD+BDIIaPIFvg1uCU4JUApdHCIFgg3aIX4Eygh+BP?= =?us-ascii?q?Ic2hQCEHIZbDwMegQQcggozGiOBAIISgXA8gQUBAoJIgT6JFj0wiFSEMiuCGAE?= =?us-ascii?q?B?= X-IronPort-AV: E=Sophos;i="5.48,426,1517871600"; d="scan'208,217";a="261343491" Received: from mail-wr0-f170.google.com ([209.85.128.170]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 09 Apr 2018 11:09:28 +0200 Received: by mail-wr0-f170.google.com with SMTP id 80so8648597wrb.2 for ; Mon, 09 Apr 2018 02:09:29 -0700 (PDT) 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=utBnVEY1s/e5gSqTgf7roiEaDrgeV80Xsux/v7qH4GE=; b=f3aOTbL+yt+ud/ZEiM9W2/eOW8QA9UnSJU01BteSLSIVb486haFRGP/6CoMny8VgBd NMHZSa0GIIBx3gK63EUydoHOsXh0u2dXlYfoxOfJc1XTZsORu96fY4mTUQcPPbpLqAk9 D5N6uN6hUnvIthvEvAji7k2WKwhMdYEPsOEBgq06J1qyvNALQKilIkGdAo8B81AvRWeS cgpPbnVTCwYEHTNSwxCcLMF6O0dQcwfbzoNFxqRrUdA5iwrJ5mDXPZfq8fdDg+NlMdil bDTvhXQqLrfQLmzaXFG9EvYhmHGy7wQ18L4vlxMLWgtJAnPZOBjzieQr637GTsuaVKH2 YLtw== 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=utBnVEY1s/e5gSqTgf7roiEaDrgeV80Xsux/v7qH4GE=; b=W7fXl4+uWcoBi6zRB4FPU6C0s9E/d6etCjmAAwDHBlPwepXm3/xoupaINAanNpio+g zSIouUezQVcPrRgowMdLa8o+nhjXMLVg0g2+cFjCBaVZjROfE5YUdukpc0rvzR0/1TIA FVyEGbJvdCHOeaJOCUugateQSSiTygiiErw5IGd7wJhF1WQROCYQuepShOJiOHC+7W0H PEf2+Qt5d0h6JHMxSPHjamGrO62+lQG+Uxwq7wXPVgggXgjzrK1cNH8mxWSzayHusBHh KMru0M9RTeyjOVHOvKEneDvgSs/YaCiRj8ii/4/s3IhTdQGt/M+/61aavhRIOsdlgPMM rZ4g== X-Gm-Message-State: AElRT7FX2ffIFVHZA/8lFe3e5fnv+GDtJQzcIP5qRulklX8vfnlOqYDF IlqUp4fSVrd3ZfhcOskfO/4dRkT5HrDJ4z+V2bSW/d3b X-Google-Smtp-Source: AIpwx48aAze/Df+I78gb7JODrugzfsnA/VW1lwh4OZI4lMt6sm92NdDl+qiRm6nGs7ILZPq8HPsfC+yfD6E6uTZJigg= X-Received: by 10.223.163.195 with SMTP id m3mr26876642wrb.91.1523264967912; Mon, 09 Apr 2018 02:09:27 -0700 (PDT) MIME-Version: 1.0 Received: by 10.28.229.145 with HTTP; Mon, 9 Apr 2018 02:09:07 -0700 (PDT) From: David Baelde Date: Mon, 9 Apr 2018 11:09:07 +0200 Message-ID: To: OCaml Mailing List , haskell@haskell.org Content-Type: multipart/alternative; boundary="f403045f20164fb25f056966c33c" Subject: [Caml-list] EPIT 2018 Software Verification Spring School, last call Reply-To: David Baelde X-Loop: caml-list@inria.fr X-Sequence: 16789 Errors-to: caml-list-owner@inria.fr Precedence: list Precedence: bulk Sender: caml-list-request@inria.fr X-no-archive: yes List-Id: List-Archive: List-Help: List-Owner: List-Post: List-Subscribe: List-Unsubscribe: --f403045f20164fb25f056966c33c Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable EPIT 2018 Software Verification Spring School Last call for participation : ** Pre-registration closes on April 13th. ** Please pre-register now (it takes 1 mn), ** validate and pay later. ** Full program announced. =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=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=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D When: May 7-11, 2018 Where: Centre Paul-Langevin in Aussois, France Web: https://projects.lsv.fr/epit18/ =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=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=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D EPIT (=C3=89cole de Printemps en Informatique Th=C3=A9orique) is a long ser= ies of Spring schools in theoretical computer science, initiated by Maurice Nivat in 1973. Since then, it has covered various fields of computer science, and has been a key event where young researchers meet. The theme of the 2018 school is software verification. The need for software verification in our information society has been recognized as early as in the =E2=80=9970s and it is an ever-more-important concern today. Over the past decades, it has driven exciting research in various fields of theoretical computer science such as logic, automata, type systems, algorithms and complexity. Recently, verification techniques have seen rapid development and industrial adoptions, notably following the SMT revolution. The school will cover several fundamental aspects of software verification through four lectures (6h each): =E2=80=93 SMT solvers, by Pascal Fontaine (LORIA) =E2=80=93 Program verification with F*, by C=C4=83t=C4=83lin Hri=C5=A3cu (I= nria Paris) =E2=80=93 Bounded model-checking, by Gennaro Parlato (Uni. of Southampton) =E2=80=93 Concurrent program logics, by Viktor Vafeiadis (MPI Kaiserslauter= n) and four research talks (1h each): =E2=80=93 SMT, String and Security, by Philipp R=C3=BCmmer (Uppsala Univers= ity) =E2=80=93 Verification of invariants for convergent replicated data types, by Gustavo Petri (Universit=C3=A9 Paris Diderot) =E2=80=93 Traces, interpolants, and automata : Ultimate Automizer's approach to software verification, by Matthias Heizmann (University of Freiburg) =E2=80=93 F* and security, by Antoine Delignat-Lavaud (Microsoft Research Cambridge) Please find more information, e.g. regarding the venue and registration, on our website: . Pre-register immediately, and spread the word! =E2=80=94 The organizers, David Baelde (LSV, ENS Paris-Saclay & Inria Paris) Constantin Enea (IRIF, Universit=C3=A9 Paris Diderot) --=20 Caml-list mailing list. Subscription management and archives: https://sympa.inria.fr/sympa/arc/caml-list Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs= --f403045f20164fb25f056966c33c Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable

EPIT 2018 Software Verification Spring School

L= ast call for participation :

=C2=A0 ** Pre-registration closes on Ap= ril 13th.
=C2=A0 ** Please pre-register now (it takes 1 mn),
=C2=A0 *= * validate and pay later.

=C2=A0 ** Full program announced.

= =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=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=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D

=C2=A0 Whe= n: May 7-11, 2018
=C2=A0 Where: Centre Paul-Langevin in Aussois, France<= br>=C2=A0 Web: https://projects= .lsv.fr/epit18/

=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=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=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D

EPIT (=C3=89cole de Printemps en Informatique Th=C3=A9oriq= ue) is a long series
of Spring schools in theoretical computer science, = initiated by
Maurice Nivat in 1973. Since then, it has covered various f= ields of
computer science, and has been a key event where young research= ers
meet.

The theme of the 2018 school is software verification. = The need for
software verification in our information society has been r= ecognized
as early as in the =E2=80=9970s and it is an ever-more-importa= nt concern
today. Over the past decades, it has driven exciting research=
in various fields of theoretical computer science such as logic,
aut= omata, type systems, algorithms and complexity. Recently,
verification t= echniques have seen rapid development and industrial
adoptions, notably = following the SMT revolution.


The school will cover several fund= amental aspects
of software verification through four lectures (6h each)= :

=E2=80=93 SMT solvers, by Pascal Fontaine (LORIA)
=E2=80=93 Pro= gram verification with F*, by C=C4=83t=C4=83lin Hri=C5=A3cu (Inria Paris)=E2=80=93 Bounded model-checking, by Gennaro Parlato (Uni. of Southampton= )
=E2=80=93 Concurrent program logics, by Viktor Vafeiadis (MPI Kaisersl= autern)

and four research talks (1h each):

=E2=80=93 SMT, Str= ing and Security, by Philipp R=C3=BCmmer (Uppsala University)
=E2=80=93 = Verification of invariants for convergent replicated data types,
=C2=A0 = by Gustavo Petri (Universit=C3=A9 Paris Diderot)
=E2=80=93 Traces, inter= polants, and automata :
=C2=A0 Ultimate Automizer's approach to soft= ware verification,
=C2=A0 by Matthias Heizmann (University of Freiburg)<= br>=E2=80=93 F* and security,
=C2=A0 by Antoine Delignat-Lavaud (Microso= ft Research Cambridge)


Please find more information, e.g. regard= ing the venue and
registration, on our website:

=C2=A0 <https://projects.lsv.fr/epit18/&g= t;.

Pre-register immediately, and spread the word!

=E2=80=94<= br>
The organizers,
David Baelde (LSV, ENS Paris-Saclay & Inria P= aris)
Constantin Enea (IRIF, Universit=C3=A9 Paris Diderot)

--f403045f20164fb25f056966c33c--