[hacs] DeepSpec Summer School on Verified Systems -- apply now!

[Adam Chlipala]

Hello HACSers,

At the last workshop, some of you expressed interest in learning more 
about the Coq theorem prover.  To that end, the following summer school 
may be of interest.  Please feel free to contact me personally if you 
have any questions about it.


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


        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 
visithttp://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://moderncrypto.org/mail-archive/hacs/attachments/20170213/295e740f/attachment.html>