[Cryptography] Fw: DeepSpec Summer School on Verified Systems -- apply now!

Perry E. Metzger perry at piermont.com
Tue Jan 31 12:33:59 EST 2017


[I believe this topic is of substantial interest to readers of this
list. Formal verification, once seen as an impossible goal, is
now rapidly becoming a real software engineering tool, and I think it
will transform both our protocols and our implementations. This is
an unparalleled opportunity to learn about it. --Perry]

Begin forwarded message:

Date: Mon, 30 Jan 2017 16:54:12 -0500
From: "Benjamin C. Pierce" <bcpierce at cis.upenn.edu>
To: types-announce at lists.seas.upenn.edu, csf-attendees at mail-infsec.cs.uni-saarland.de, deepspec at lists.cs.princeton.edu, coq-club at inria.fr, ecoop-info at ecoop.org, dsllab <dsllab at lists.seas.upenn.edu>
Subject: DeepSpec Summer School on Verified Systems -- apply now!

The first DeepSpec Summer School on Verified Systems will be held in
Philadelphia from July 17 to 28, 2017, preceded by an introductory
Coq Intensive from July 13 to 15.  Applications are now open:

     http://deepspec.org/events/ss17detail.html
     <http://deepspec.org/events/ss17detail.html>.

Overview

Can critical systems be built with no bugs in hardware, operating
systems, compilers, crypto, and other key components?  It may seem a
pipe dream, but the past decade has seen remarkable advances in the
technology required to realize it.

This summer school aims to give participants a wide-ranging overview
of several ambitious projects currently underway in this space.
Participants will gain a thorough understanding of the conceptual
underpinnings of these projects plus considerable hands-on experience
with the state-of-the-art tools being used to build them.

Dates

The summer school will open with a three-day intensive course on the
fundamentals of the Coq proof assistant, for participants who are new
to Coq. The main lectures take place during the weeks of July 17 and 24.

Lecturers and Topics

Andrew Appel            Verified functional algorithms
Adam Chlipala           Program-specific proof automation
Frans Kaashoek & Nickolai Zeldovich     Certifying software with crashes
Xavier Leroy            The structure of a verified compiler
Benjamin Pierce         Property-based random testing with QuickChick
Zhong Shao              CertiKOS: Certified kit operating systems
Stephanie Weirich       Language specification and variable binding
Steve Zdancewic         Vellvm: Verifying the LLVM

More information

To apply, or for more information, please visit
  http://deepspec.org/events/ss17detail.html
 <http://deepspec.org/events/ss17detail.html>.

Applications received by Feb 15 will be given equal consideration;
applications received after Feb 15 will be considered on a space- and
funds-available basis.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.metzdowd.com/pipermail/cryptography/attachments/20170131/48078a6f/attachment.html>


More information about the cryptography mailing list