coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Colocated with PLDI: Workshop on Deep Specifications in the Wild

From: Adam Chlipala <adamc AT csail.mit.edu>
To: coq-club AT inria.fr, types-announce AT lists.seas.upenn.edu
Subject: [Coq-Club] Colocated with PLDI: Workshop on Deep Specifications in the Wild
Date: Thu, 15 Jun 2017 05:54:28 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=adamc AT csail.mit.edu; spf=Pass smtp.mailfrom=adamc AT csail.mit.edu; spf=None smtp.helo=postmaster AT outgoing-stata.csail.mit.edu
Ironport-phdr: 9a23:N/miyxL5xrRr8KAiftmcpTZWNBhigK39O0sv0rFitYgXKv/zrarrMEGX3/hxlliBBdydsKMbzbKO+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZPebgFKiTanfb9+MAi9oBnMuMURnYZsMLs6xAHTontPdeRWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjTbxFFzsmKHw65NfqtRbYUwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr86QzSi67pgRgHuhikJKjU19HjbhtF0ga5eph+quh5xzJPOYIyNKvRwfr7Tc9AUS2VPUcleSzdMDZmgY4YVFecNIehVoov7qlATrRW+Hw6sBOb3xzJUm3D5x6g62Pk/HAHG2AwgHsoOv27QrNrvKawfVvq6w7TSwjXGc/xbwivy6JPSfRAgpfGAR7dwccvNyUU1CQzKk0iQpJXjMjiI2OoNtG2b4PBhVeKpk2Mnqxtxojy1ysgwjYnJg5oZykvF9SV22IY1Ice3SEhhbd6jCptQuDmWN41xQsMtQmFovjw2yrocuZ60ZCQF1YooyADHa/yca4iH/A7sWPyWITdii3JpYL2/hxG18Uivzu3zSNO430pNripAitXDq2oC1wbL6sedUPd9+0ah2TKX2w/J7+FLO0E1la3dK5I73rEwkZ8TvVzbHi/smUX2irOZeVs4+uiv7eTreKvpqYKBN4Nslg7+MqAums2nAesiNggBRXKX+eKi273/5UH5XK9FjuAqkqnCrJ/aJcIbpq+2AwNP1IYs9Qq/AjG729obhXkKNE9JdAyEgoTzNVzCPOr0Aemlj1iyjTtn2+jKM737DpnQIXXOk63tcatj50Nd0gY/0N9S6pZSB7ocOvz8QFXxu8bdDhIhMwy73eLnCNJl24MZRGKPHqCZMKTTsV+O6eIjOvKMZJMPtzbhMfcp/eLhjWQjll8ceamlx54XaHGkHvh8PUqWfGfsjs8AEWcMoAU+UPTnhECcXTNQfXq/Ub4w6islBI68E4vPW5yhjKSE3CihH51WYm5GCkqLEXftb4iLQeoDZziXIsB9iTELSaOhRJUg1RGqrgP6zrtnLvbO9iIGqJ3jycB55/fPmhEq6Tx0E8Od3nmRQGFzh2MEXiM53KRioUNm0VqDyqh5g/lAFdNJ/f9JUwE6NYTdz+NgEdzyVBjBLZ+1TwOtRczjCjUsRPowxcUPagBzAZHqkgHb0jHvCrkTkKGND5Ec9qPHw2O3PMt00DDbzKQniR8rTtYcG3ehg/tW+wHWT6XJl0SBnqKjPfAV0CfI/0+I1mOPuAddURI2XKnYCyNMLnDKpMj0sxuRB4SlDq4qZ04YmMM=

Those of you attending PLDI in Barcelona next week may be interested in also attending a workshop (on Thursday, after PLDI proper ends) run by our DeepSpec Project.

The workshop web site: http://pldi17.sigplan.org/track/dsw-2017-papers
The more general project web site: https://deepspec.org/

Briefly, our project is about scaling proof-assistant-based formal methods to more significant systems, especially through reuse of well-specified components. A large element of the project is education and community-building, hence this workshop!

We have a speaker line-up that combines industry early-adopters of formal methods with some of our project leaders. Full schedule information is on our workshop web site, but here is an overview.

Invited Speakers from Industry

Aleksey Nogin from HRL, on integrating formal-methods tools in the DARPA HACMS program
Dominic Rizzo from Google, on applying proof assistants to cryptography at Google
Michael Tautschnig from Amazon, on static analysis of hypervisor code

Speakers From the DeepSpec Project

Andrew W. Appel from Princeton, on verifying concurrent C programs with the Verified Software Toolchain
Lennart Beringer from Princeton, on verifying cryptographic C code with the Verified Software Toolchain
Adam Chlipala from MIT, on generating low-level cryptographic code automatically from specifications
Zhong Shao from Yale, on verifying the CertiKOS hypervisor OS kernel

[Coq-Club] Colocated with PLDI: Workshop on Deep Specifications in the Wild, Adam Chlipala, 06/15/2017