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 E35F08239C for ; Tue, 28 Nov 2017 11:27:17 +0100 (CET) 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-wm0-f50.google.com Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of david.baelde@gmail.com) identity=pra; client-ip=74.125.82.50; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="david.baelde@gmail.com"; x-sender="david.baelde@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of david.baelde@gmail.com designates 74.125.82.50 as permitted sender) identity=mailfrom; client-ip=74.125.82.50; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="david.baelde@gmail.com"; x-sender="david.baelde@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-wm0-f50.google.com) identity=helo; client-ip=74.125.82.50; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="david.baelde@gmail.com"; x-sender="postmaster@mail-wm0-f50.google.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3Ag91GXxQArNNCgr7Ljq2lEA7yPdpsv+yvbD5Q0YIu?= =?us-ascii?q?jvd0So/mwa64ZBaN2/xhgRfzUJnB7Loc0qyN7PCmBDRIyK3CmU5BWaQEbwUCh8?= =?us-ascii?q?QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnY6Uy/yPgtt?= =?us-ascii?q?J+nzBpWaz4Huj7jzqNXvZFBvrzO4ZftXJRSyrAPe/u0Xmpcqfq04zx+MpnpTZ8?= =?us-ascii?q?xXw3lpLBSdhUCvyN23+ctP+jpRt7oL/sNEXaiyK6gxU71USj4vPmQ56eXksBDC?= =?us-ascii?q?SU2E4X5KATZeqQZBHwWQtEKyZZz2qCav87MlgCQ=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0A2BABrOR1afzJSfUpcHQIdB4NRAT5uJ?= =?us-ascii?q?weDNUOBNpd+i1SHTYVKghEKBRqBYoM6hHoHQRYBAQEBAQEBAQEBEgEBCQsLCCY?= =?us-ascii?q?xgjgFAR4BBYJQFx0BGx4DEgMGBzcCJAERAQUBIoocAQMVigqNVoNFQIwQggUFA?= =?us-ascii?q?RyDCgWDWAoZJw1YgmcMHgIBBRKDKIIHgVWBaYI1gj+EAIJogmMFokmCN4U7jRq?= =?us-ascii?q?Ff41QhkOGNIk0FAUfgRYmDIF2MhojgQCBd4JegXhANohEgVgBAQE?= X-IPAS-Result: =?us-ascii?q?A0A2BABrOR1afzJSfUpcHQIdB4NRAT5uJweDNUOBNpd+i1S?= =?us-ascii?q?HTYVKghEKBRqBYoM6hHoHQRYBAQEBAQEBAQEBEgEBCQsLCCYxgjgFAR4BBYJQF?= =?us-ascii?q?x0BGx4DEgMGBzcCJAERAQUBIoocAQMVigqNVoNFQIwQggUFARyDCgWDWAoZJw1?= =?us-ascii?q?YgmcMHgIBBRKDKIIHgVWBaYI1gj+EAIJogmMFokmCN4U7jRqFf41QhkOGNIk0F?= =?us-ascii?q?AUfgRYmDIF2MhojgQCBd4JegXhANohEgVgBAQE?= X-IronPort-AV: E=Sophos;i="5.44,467,1505772000"; d="scan'208,217";a="246333934" Received: from mail-wm0-f50.google.com ([74.125.82.50]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 28 Nov 2017 11:27:17 +0100 Received: by mail-wm0-f50.google.com with SMTP id 124so736542wmv.1 for ; Tue, 28 Nov 2017 02:27:17 -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=/HUIwpqGcdINNR4yw3rp9NsYcqOVb0mkxXKew7U2SWs=; b=eYMQmmHW5/0xHXHFX3AQ2eQ/uuL5YPSqgxFxmP+AmhenyvP4kXXdytR03xtATUZTjG lGomxiNXjIWUz3HJtDGyrQL2t7xXW7l8BEuvnP7fz7dJKRvwk90V/N/ffGCxoALpt9HY 5Lo8K7tajTlKSZ+HlLxW0ewDp4qQm5HSKpSWmvsGh0/hPhMgdkBj0zfcnYFVcvXPPJdT uFJkHWykONkSWNqk8Xpb412rLxH0KYdSzFdmgiDFrqUqlc9A86A9DPM7GbIxQ4KiSaUo dLeDIA7fuw2xq+fv+M/nhURyjoV6ykWllNUnWLIkDGWp3Ai0xoudD87B7WBEixin9Tm1 FHXA== 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=/HUIwpqGcdINNR4yw3rp9NsYcqOVb0mkxXKew7U2SWs=; b=tPDDs3vzfAm/RV/qxirPKyXrP24/kkz3PJ6UkdBBIF44Ch0rQkviZzd31y9jTe4g+b nD0TRQnWyKGhnhpA09tx+6eHfzU8aXBGmQUoLXjmK8YE/WMmMZ8rLY+0z9G4RkdDeXCH sD+c+xZ2+WRNLujJDCdXUvs2LQDwGYsPjcCZElgm1R4wZBXu63A54QExszhwtE0HWqZK oaHHAxGDSu9y6qXgAjDhRWF88u/1+nC1M3HEdYA2IkBpQnmuViAMxl2fGNLylAhq+zv2 mifteCRaIlavLk7Agw9RBDdXt0w9DgPaVhMbhMVQ6PJxG9CiusWCck+CRMzEXJ9pIcOU Ej3A== X-Gm-Message-State: AJaThX5bdfvE2sIJra5HZovqYSbk6mNj1AD3FilJd8fN8s3qlQmYYR7w f8pkhbXj/27OXLxx6JUW802DHAvib392TZy3/lkW1rEU X-Google-Smtp-Source: AGs4zMZ7fPz4StecMmth+RRbvRPUQZ1AjNjsollRyFoWNYIGViEP9+vXxUU4fULvSrkMjnDTHciRLyT1hh+jjcKy8Fg= X-Received: by 10.28.175.132 with SMTP id y126mr17687295wme.20.1511864836499; Tue, 28 Nov 2017 02:27:16 -0800 (PST) MIME-Version: 1.0 Received: by 10.28.46.132 with HTTP; Tue, 28 Nov 2017 02:26:56 -0800 (PST) From: David Baelde Date: Tue, 28 Nov 2017 11:26:56 +0100 Message-ID: To: OCaml Mailing List Content-Type: multipart/alternative; boundary="001a11443d3a872f57055f087606" Subject: [Caml-list] EPIT 2018 Software Verification Spring School, first CfP --001a11443d3a872f57055f087606 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable EPIT 2018 Software Verification Spring School =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 EPIT (=C3=89cole de Printemps en Informatique Th=C3=A9orique) is a long series 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: =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 (University of Southam= pton) =E2=80=93 Concurrent program logics, by Viktor Vafeiadis (MPI Kaiserslauter= n) More information may be found on our website . Details such as registration will be announced later. Spread the word and save the date! =E2=80=94 The organizers, David Baelde (LSV, ENS Paris-Saclay) Constantin Enea (IRIF, Universit=C3=A9 Paris Diderot) --001a11443d3a872f57055f087606 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable

EPIT 2018 Software Verification Spring School

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

EPIT (=C3=89cole de Printemps en Informatique
Th=C3=A9orique) is= a long series of Spring schools in
theoretical computer science, initia= ted by Maurice
Nivat in 1973. Since then, it has covered various
fiel= ds 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 reco= gnized 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, notab= ly following the SMT revolution.

The school will cover several funda= mental aspects
of software verification:

=E2=80=93 SMT solvers, b= y Pascal Fontaine (LORIA)
=E2=80=93 Program verification with F*, by C= =C4=83t=C4=83lin Hri=C5=A3cu (Inria Paris)
=E2=80=93 Bounded model-check= ing, by Gennaro Parlato (University of Southampton)
=E2=80=93 Concurrent= program logics, by Viktor Vafeiadis (MPI Kaiserslautern)

More infor= mation may be found on our website
<https://projects.lsv.fr/epit18/>. Details such as
regi= stration will be announced later.

Spread the word and save the date!=

=E2=80=94

The organizers,
David Baelde (LSV, ENS Paris-Sa= clay)
Constantin Enea (IRIF, Universit=C3=A9 Paris Diderot)

--001a11443d3a872f57055f087606--