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 46DBF5D4 for ; Thu, 27 Feb 2020 19:44:12 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.70,493,1574118000"; d="scan'208";a="437953133" Received: from sympa.inria.fr ([193.51.193.213]) by mail2-relais-roc.national.inria.fr with ESMTP; 27 Feb 2020 20:44:11 +0100 Received: by sympa.inria.fr (Postfix, from userid 20132) id 2A8397ED20; Thu, 27 Feb 2020 20:44:11 +0100 (CET) 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 1A8377ED20; Thu, 27 Feb 2020 01:01:27 +0100 (CET) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=shankar@csl.sri.com; spf=Pass smtp.mailfrom=shankar@csl.sri.com; spf=Pass smtp.helo=postmaster@GCC02-DM3-obe.outbound.protection.outlook.com IronPort-PHdr: =?us-ascii?q?9a23=3AxVmHzBwPjMIbQpTXCy+O+j09IxM/srCxBDY+r6Qd?= =?us-ascii?q?2uwSIJqq85mqBkHD//Il1AaPAdyHraMZwLOG+4nbGkU+or+5+EgYd5JNUxJXwe?= =?us-ascii?q?43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRp?= =?us-ascii?q?OOv1BpTSj8Oq3Oyu5pHfeQpFiCeybL9oKBi7rQrdutQVjIB/Nqs/1xzFr2dHdO?= =?us-ascii?q?hR2W5mP0+YkQzm5se38p5j8iBQtOwk+sVdT6j0fLk2QKJBAjg+PG87+MPktR/Y?= =?us-ascii?q?TQuS/XQcSXkZkgBJAwfe8h73WIr6vzbguep83CmaOtD2TawxVD+/4apnVAPkhS?= =?us-ascii?q?EaPDE+7WHXjNF/jKNAoB29oxx/xJXUb5+IO/Fjeq/Qcs8WSW9HU81MVSJOH5m8?= =?us-ascii?q?YpMSAeQBM+ZWrIfzqFUBohS8GQaiC/jiyiNLi3LswaE2z+osHAPA0Qc9H9wOqn?= =?us-ascii?q?PUrNDtOakKS++10LPHzS/ZYPNUwzj97pXDfA0hof6WW7JwctDeyVMyHA7ClVWQ?= =?us-ascii?q?qZbqPzWW1usXqWiW9PZvVfmri2I9sAFxuDmvyt0whYnOg4IY01bJ/jh3zoYyIN?= =?us-ascii?q?23Uk97Ydi8HZtLrSGaNpF6Td8lQ2FtoCo6yKcJuJ6gcygN05Qo3Rvfa/2HcoeS?= =?us-ascii?q?+B7sSOGRITJ+iXl4e7y/nw6//Ee8xuHmS8W4zFRHojBBn9XRrHwA1AHf5tCaRv?= =?us-ascii?q?dj/UqtwyuD2gPJ5u1aIU04ibDXJ4Mvz7M/kJcYrF7NETXsmErsia+bbkUk9fas?= =?us-ascii?q?6+Tgerjop4GROpFohg3gK6gglMuxDOohPggJRGeU5/6w1Lr+/U3lW7pKieA2kq?= =?us-ascii?q?/Ev5zAPcQbvKm5AxNL3Yk/9xa/DjCm0NICkXkAMVJFZBaHj4/uO1HNOvz3EfC/?= =?us-ascii?q?g1G0nDdqwfDJIKHhD43CI3TfirvtYKpx5kxGxAc30NxT/ZFZBqwZLPL2QEDxtd?= =?us-ascii?q?jYDhEjMwyzxubqEM591oMEVmKJAa+WKrnSvESU6eI0J+mAfpQVuCz8K/Q/+/Hu?= =?us-ascii?q?ino5lUcHfaa1xZsXdGy4HvN+LkqFe3Xsh9MBHX4Ovgo/V+zqlEaPUSVTZna3R6?= =?us-ascii?q?Iz/Cs3CIOgDYfZR4CimqaN3CmhHpdOfGBJFkiMEWv0d4WDQ/oDdCWSItZ4njMY?= =?us-ascii?q?UbihVpQu2Aq1tA76zrpnNvDb9jcZtZLlzth15vfcmQs89TxuXIyh1DSQSW11hW?= =?us-ascii?q?gMQCQ70OVlrEd80laO17Rj0bQLRvJJ4PYcdA4mPITVzeV8Q+vyUwTCd83BHE2m?= =?us-ascii?q?S9OlCCsZRck1hcQUYgB2HND03UOL5DajH7JAz+/DP5cz6K+JgyCoe5RNjk3e3a?= =?us-ascii?q?xktGEIB9NVPDT91KVk807IHY+PmEKcxf7zKPYsmRXV/WLG9lKg+UFVVAksDvfq?= =?us-ascii?q?dltHPA76iI+84UnPCbizFb4gLw1Nj9aYLbdHYcHoilMAQ+r/PNPZYCS6nGLiXE?= =?us-ascii?q?/ZlIPJV5LjfiAm5AuYDUEFlw4J+nPfblo1HSPnuHjfSjdpEAC2bg=3D=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0AtNgBcBldeh1FbayhmHAEBASgBBwEBA?= =?us-ascii?q?QUBBAQBAQIBBwEBgVWBPgISKSdWG3UDBzKEFINHAQGBEIQqhSqZEoFhglIDVAk?= =?us-ascii?q?BAwEKAQEjDAQBAYFMgnQCTAmBSQYBBDQTAhABAQUBAQECAQIDBAETAQEBCA0JC?= =?us-ascii?q?CmFPgsBgjsMGoJ6CQIBAxIRDwEFCAEBOA8JHAIfBwICVwwBBggBAR45gksBgko?= =?us-ascii?q?DLgECDJN7kGcCAoE3iGEBAXSBMoJ/AQEFgS8BgRSCTxiCDAkJAYEEKAIBAYt9Q?= =?us-ascii?q?IIAEoEmD4FxNwUCgXABgUYZAQKBO4M6FIJKjXaKLZd3gkaCUYUAjw4ifI4PjCO?= =?us-ascii?q?XbIUwjRsCBAIEBQIOAQEEAYFpgUgBGgEOCDMaCBsVgVkKgRABAQExCUcYDY41A?= =?us-ascii?q?h5vAQKCSYpUIlMCAYxbLYIWAQE?= X-IPAS-Result: =?us-ascii?q?A0AtNgBcBldeh1FbayhmHAEBASgBBwEBAQUBBAQBAQIBBwE?= =?us-ascii?q?BgVWBPgISKSdWG3UDBzKEFINHAQGBEIQqhSqZEoFhglIDVAkBAwEKAQEjDAQBA?= =?us-ascii?q?YFMgnQCTAmBSQYBBDQTAhABAQUBAQECAQIDBAETAQEBCA0JCCmFPgsBgjsMGoJ?= =?us-ascii?q?6CQIBAxIRDwEFCAEBOA8JHAIfBwICVwwBBggBAR45gksBgkoDLgECDJN7kGcCA?= =?us-ascii?q?oE3iGEBAXSBMoJ/AQEFgS8BgRSCTxiCDAkJAYEEKAIBAYt9QIIAEoEmD4FxNwU?= =?us-ascii?q?CgXABgUYZAQKBO4M6FIJKjXaKLZd3gkaCUYUAjw4ifI4PjCOXbIUwjRsCBAIEB?= =?us-ascii?q?QIOAQEEAYFpgUgBGgEOCDMaCBsVgVkKgRABAQExCUcYDY41Ah5vAQKCSYpUIlM?= =?us-ascii?q?CAYxbLYIWAQE?= X-IronPort-AV: E=Sophos;i="5.70,490,1574118000"; d="scan'208";a="340539979" X-MGA-submission: =?us-ascii?q?MDFCnq0FYfvScGkJkt/WEgFLaTV5XPb6QSGy/b?= =?us-ascii?q?U7ZvPjyOd1YcNfcGliddPGBMjuKulDzsB006Fooq+OHkDkmApgR2Y5lB?= =?us-ascii?q?sbmUb8BQhuHueJ1z+MKLWG97u8i2OBdQ+BwMN+2F0p1PAKLIMaK3SRWq?= =?us-ascii?q?pgtdB5sL58T/5xjk31T3rxhA=3D=3D?= Received: from mail-dm3gcc02on2081.outbound.protection.outlook.com (HELO GCC02-DM3-obe.outbound.protection.outlook.com) ([40.107.91.81]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/AES256-GCM-SHA384; 27 Feb 2020 01:00:47 +0100 ARC-Seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=S41BD7aBmy3hc3E0cMJkLb8tI7mMapfrYJiC8hJXbBdLSCMzMmIoV3Q3HF+zPK8kgI9qxkwsQPVQcDJV+s8/PoO9FeAKWSobIU3NrdiXg3Nup9bBPnyqQAzCDYwNSJAJ8HF5+/l82K/Ysz2HLsBy0XNtyxuEMuapF6D4A1qTiGVnZ6xmBwPnOzQdGL0lthxIj5qKQKK8h5KW5PXWP006/eHZd7JNwt+oV5c2jx86CUIKBVeDBc5lcePQx9HoEJyWYxtHZ27aS0jq7J4gjasGApFDevc/f9GP+UH5kU2SGEIf9M3bk3oe7B9rtRCiFzHO3OMwEfqv5mVbaung3kIiog== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=rnIE7+IeArbrVQsMqgtj5r7Wxe+k8jEuMHMAyBARnXc=; b=cINtiPy219BG0kIiOAehqzS0fvaEfAm2YR/TpyF6GyWg3zvJprPSMvi4pUVnVn+1siyldUN5puTqjNxadBmTjEu4SWtF72zVY7UaZPV+Q6vh5l30DiJsaNCOeOfoO76BtCRhr/oGK2vwqfU51kdxWk43v1d1CQMsIZShPH8SHBq48tTggW0MyLv/E4lq+c8tasvovEPjnv78UbfcYvu5UaoO4OcNlHodCAczK17/g36tS6YYBF+a5P3rkD6i4thtETX0B+yazBCt2Cq9BZWjij/TwbwePYQqSaiPlnHV8E9ZdhZzbQYOaUsA+/Yv6CTVxS+DMqHc7FmbzPZ+sZs0Ww== ARC-Authentication-Results: i=1; mx.microsoft.com 1; spf=pass (sender ip is 128.18.241.12) smtp.rcpttodomain=gnu.org smtp.mailfrom=csl.sri.com; dmarc=pass (p=quarantine sp=quarantine pct=100) action=none header.from=csl.sri.com; dkim=pass (signature was verified) header.d=csl.sri.com; arc=none DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=sriit.onmicrosoft.com; s=selector2-sriit-onmicrosoft-com; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=rnIE7+IeArbrVQsMqgtj5r7Wxe+k8jEuMHMAyBARnXc=; b=gZi1cnmJvwHFrC1v8Q21dy5e2IJf0pGjQCsdMS67lDJMierY/dt/W/Wt8FULjAUbGiio3AiYAKy8AB0q/dfBOgOUZRVDl6j2lAzqEVPv1T3q7z8lJnGKwgdycQ1F5albEfWAVdNxYcuVYWTERXvKnZynjlXiSXWchncYdZ1smR0= Received: from CY4PR09CA0008.namprd09.prod.outlook.com (2603:10b6:910:2::18) by BY5PR09MB3858.namprd09.prod.outlook.com (2603:10b6:a03:1ff::24) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.2772.14; Thu, 27 Feb 2020 00:00:40 +0000 Received: from DM3GCC02FT011.eop-gcc02.prod.protection.outlook.com (2a01:111:f400:7d04::207) by CY4PR09CA0008.outlook.office365.com (2603:10b6:910:2::18) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.2772.15 via Frontend Transport; Thu, 27 Feb 2020 00:00:40 +0000 Received: from itmp-smtprelay.sri.com (128.18.241.12) by DM3GCC02FT011.mail.protection.outlook.com (10.97.8.210) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.2750.18 via Frontend Transport; Thu, 27 Feb 2020 00:00:40 +0000 Received: from mx-dkim-out.csl.sri.com (f5-30-fip.sri.com [128.18.30.110]) by itmp-smtprelay.sri.com (Postfix) with ESMTPS id 2E8335F952; Wed, 26 Feb 2020 16:00:39 -0800 (PST) Received: from mxzero.csl.sri.com (mxzero.csl.sri.com [130.107.1.30]) by mx-dkim-out.csl.sri.com (8.15.2/8.15.2/Debian-3) with ESMTP id 01R00YLX000786; Wed, 26 Feb 2020 16:00:35 -0800 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=csl.sri.com; s=mail20190530; t=1582761639; bh=2dkdbn/YS/1qgsnsczAqzjESBUrOx59js2JVbmzWozY=; h=Subject:From:References:Date:To:In-Reply-To; b=jD2PnH8Swmksz+6Pbcb4Bj7PE0NdrSr05/Uo23olxY/K4eil14L8QGWpqIy9RRJk+ FPIks4rsHYGmPqGMPAKkRLLDaSUPWXaqUXT1Fx+BeC1xMm3AUlJzFQsI696Zuqazj9 R2TPgSKJniMWdPJ0iF3bbahoxdgkkKJG2Lv9H3sE= Received: from mx3.csl.sri.com (mx3.csl.sri.com [130.107.1.31]) by mxzero.csl.sri.com (8.14.4/8.14.4/Debian-4.1ubuntu1.1) with ESMTP id 01R002vJ013496 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-GCM-SHA384 bits=256 verify=NOT); Wed, 26 Feb 2020 16:00:03 -0800 Received: from [128.18.250.134] (csl-cas15859.sri.com [128.18.250.134]) (authenticated bits=0) by mx3.csl.sri.com (8.14.4/8.14.4/Debian-2ubuntu2.1) with ESMTP id 01R000sb025961 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES128-SHA bits=128 verify=NOT); Wed, 26 Feb 2020 16:00:00 -0800 From: Natarajan Shankar References: <5A9832E8.3020003@csl.sri.com> <0e5c7eb9-65d3-96fe-6ca9-4259841bf175@csl.sri.com> Message-ID: <9eb14ee9-e10b-ccf6-b2b1-9b290df216c4@csl.sri.com> Date: Wed, 26 Feb 2020 16:00:00 -0800 User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.13; rv:68.0) Gecko/20100101 Thunderbird/68.5.0 MIME-Version: 1.0 To: undisclosed-recipients: ; In-Reply-To: <0e5c7eb9-65d3-96fe-6ca9-4259841bf175@csl.sri.com> Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 8bit Content-Language: en-US X-EOPAttributedMessage: 0 X-Forefront-Antispam-Report: CIP:128.18.241.12;IPV:;CTRY:US;EFV:NLI;SFV:NSPM;SFS:(10009020)(376002)(346002)(39850400004)(396003)(136003)(199004)(189003)(186003)(426003)(81166006)(8676002)(8936002)(81156014)(956004)(26005)(336012)(2616005)(356004)(31686004)(31696002)(86362001)(316002)(966005)(478600001)(70586007)(7366002)(6706004)(70206006)(109986005)(7406005)(2906002)(45080400002)(5660300002)(7416002);DIR:OUT;SFP:1101;SCL:1;SRVR:BY5PR09MB3858;H:itmp-smtprelay.sri.com;FPR:;SPF:Pass;LANG:en;PTR:InfoDomainNonexistent;A:1;MX:1; X-MS-PublicTrafficType: Email X-MS-Office365-Filtering-Correlation-Id: 66853b15-f205-422c-e3db-08d7bb1814fa X-MS-TrafficTypeDiagnostic: BY5PR09MB3858: X-Microsoft-Antispam-PRVS: X-SafeList: Domain-whitelisted X-MS-Oob-TLC-OOBClassifiers: OLM:10000; X-Forefront-PRVS: 03264AEA72 X-MS-Exchange-SenderADCheck: 1 X-Microsoft-Antispam: BCL:0; X-Microsoft-Antispam-Message-Info: ztv49AKsl/rSD+75MGrHOnRYCsbSH7VwMOIkuJ7qebC/wO4PxDsgiJkp3DXanPTWU2zD/pOmBYfI0XQiMCY0dJ6n/EecY9o4CNTHwwt82BXhIu7Zf8lXZ2Rz8ufDri2K1aPoaRuJmPHDY5Ol5N2/Y9if8hi/AEIl0vZyYO9bI7yLbo0SNqBCeI5V/x1QB3yRoKn2miom9heLTUYegIG2noLoxAjgfUG529aqHCvD9XI4eNeaJZHGVpa2M8jAzeOj5AGkv1wDKXaIObhrOlZ9gQYMA6fXwA0HA+PXZP6glt+tKiO54ggzj398Q6RtcwZNqMGKJlepqGlDlJ5+n8t98xWVszmUjsIV3xeiblH+9t/yhZMyIWgqzg/3VJ8ceCDBEYmxDIVrYY8a4LtvXT1PW4yaCDEfLtN1Y6JgFGLR9oUfdA6ASI/O8qLA2tJ7+wzrcqgluMzWKgNZjQZeekNJN1CZYlqXbDy2Tn2FLJB7Dmo473Ugxe6w/eAjQwUW+tNBZC8xMx3PpJJtcFBW6Cl+wQ== X-OriginatorOrg: sri.com X-MS-Exchange-CrossTenant-OriginalArrivalTime: 27 Feb 2020 00:00:40.0331 (UTC) X-MS-Exchange-CrossTenant-Network-Message-Id: 66853b15-f205-422c-e3db-08d7bb1814fa X-MS-Exchange-CrossTenant-Id: 40779d33-79c4-4626-b8bf-140c4d5e9075 X-MS-Exchange-CrossTenant-OriginalAttributedTenantConnectingIp: TenantId=40779d33-79c4-4626-b8bf-140c4d5e9075;Ip=[128.18.241.12];Helo=[itmp-smtprelay.sri.com] X-MS-Exchange-CrossTenant-FromEntityHeader: HybridOnPrem X-MS-Exchange-Transport-CrossTenantHeadersStamped: BY5PR09MB3858 X-Validation-by: shankar@csl.sri.com Subject: [Caml-list] Tenth Summer School on Formal Techniques, May 16-22, 2020; First FMiTF Bootcamp, May 23-28, 2020, Atherton, California Reply-To: Natarajan Shankar X-Loop: caml-list@inria.fr X-Sequence: 18026 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: Tenth Summer School on Formal Techniques , May 16 - May 22, 2020 (http://fm.csl.sri.com/SSFT20)                                                     and First Formal Methods in the Field (FMiTF) Bootcamp, May 23-28, 2020 (http://fm.csl.sri.com/SSFT20/FMiTF.html) Menlo College, Atherton, California Techniques based on formal logic, such as model checking, satisfiability, static analysis, and automated theorem proving, are finding a broad range of applications in modeling, analysis, verification, and synthesis. This school, the tenth in the series, will focus on the principles and practice of formal techniques, with a strong emphasis on the hands-on use and development of this technology. It primarily targets graduate students and young researchers who are interested in studying and using formal techniques in their research. A prior background in formal methods is helpful but not required. Participants at the school can expect to have a seriously fun time experimenting with the tools and techniques presented in the lectures during laboratory sessions. ============================================================= The lecturers at the school include: * Thomas Reps (University of Wisconsin)   Algebraic Program Analysis: Automating Abstract Interpretation * Pamela Zave (Princeton University)   Specification, Implementation, and Verification of Network Properties * J Strother Moore and Warren A. Hunt, Jr. (University of Texas)   Proving Properties of Algorithms, Hardware, and Software with ACL2 * Jose Meseguer (University of Illinois at Urbana-Champaign)   Executable Formal Specification and Verification in Maude The main lectures in the summer school start on Monday May 18 and  will be preceded by a background course on logic: * Natarajan Shankar (SRI CSL) and Stephane Graham-Lengrand (Ecole Polytechnique)   Speaking Logic ============================================================= The summer school will be immediately followed by the First Formal Methods in the Field (FMiTF) Bootcamp May 23-28, 2020 Menlo College, Atherton, CA http://fm.csl.sri.com/SSFT20/FMiTF.html The first FMitF Bootcamp will cover two themes, "Building Verified JIT Compilers" and "Formally verifying low-level programs in F*". The exercises in the Bootcamp assume that the students have a working knowledge of formal techniques. The main focus of the Bootcamp is on applying this knowledge to some domain-specific challenge problems. Lecturers  *  Emina Torlak and Xi Wang (University of Washington)     Building Verified JIT Compilers  * Jonathan Protzenko and Nikhil Swamy (Microsoft Research)    Formally verifying low-level programs in F* ============================================================= The summer school also include several distinguished invited talks. Information about previous Summer Schools on Formal Techniques can be found at http://fm.csl.sri.com/SSFT11 http://fm.csl.sri.com/SSFT12 http://fm.csl.sri.com/SSFT13 http://fm.csl.sri.com/SSFT14 http://fm.csl.sri.com/SSFT15 http://fm.csl.sri.com/SSFT16 http://fm.csl.sri.com/SSFT17 http://fm.csl.sri.com/SSFT18 http://fm.csl.sri.com/SSFT19 Jay Bosamiya of CMU has blogged about the 2018 Summer School at    https://www.jaybosamiya.com/blog/2018/05/31/ssft/ ======================================================================= You are welcome to register for one or both of the summer school and the Bootcamp.  The target audience for both events is first/second/third year graduate students in computer science.  We expect to provide support for the travel and accommodation for (a limited number of) students registered at US universities.  We welcome applications from non-US students as well as non-students (who will be admitted only if space permits).  Non-US students will have to cover their own travel and will be charged around US$800 for the summer school and $700 for the Bootcamp covering meals and lodging.  Applications should be submitted at the website http://fm.csl.sri.com/SSFT20 Applicants are urged to submit their applications before April 30, 2020, since there are only a limited number of spaces available. Non-US applicants requiring US visas are requested to apply early. We strongly encourage the participation of women and under-represented minorities in the summer school.