<html><head><meta http-equiv="Content-Type" content="text/html charset=us-ascii">
<meta http-equiv="content-type" content="text/html; charset=utf-8">
</head><body bgcolor="#FFFFFF" text="#000000" style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class="">
<div class="">
<p class="" style="box-sizing: border-box; margin: 0px 0px 10px;
color: rgb(51, 51, 51); font-family: 'Helvetica Neue',
Helvetica, Arial, sans-serif; font-size: 17px;">The first <i class="" style="box-sizing: border-box;"><span class="" style="box-sizing: border-box; font-weight: 700;">DeepSpec
Summer School on Verified Systems</span></i> will be held in
Philadelphia from July 17 to 28, 2017, preceded by an
introductory <i class="" style="box-sizing: border-box;"><span class="" style="box-sizing: border-box; font-weight: 700;">Coq
Intensive</span></i> from July 13 to 15. Applications are now open:</p>
<div class=""> <a href="http://deepspec.org/events/ss17detail.html" class="" style="font-family: 'Helvetica Neue', Helvetica,
Arial, sans-serif; font-size: 17px;">http://deepspec.org/events/ss17detail.html</a></div>
<h4 class="" style="box-sizing: border-box; font-family:
'Helvetica Neue', Helvetica, Arial, sans-serif; font-weight:
500; line-height: 1.1; color: rgb(51, 51, 51); margin-top: 10px;
margin-bottom: 10px; font-size: 21px;">Overview</h4>
<p class="" style="box-sizing: border-box; margin: 0px 0px 10px;
color: rgb(51, 51, 51); font-family: 'Helvetica Neue',
Helvetica, Arial, sans-serif; font-size: 17px;">
Can critical systems be built with <i class="" style="box-sizing: border-box;">no bugs</i> 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.</p>
<p class="" style="box-sizing: border-box; margin: 0px 0px 10px;
color: rgb(51, 51, 51); font-family: 'Helvetica Neue',
Helvetica, Arial, sans-serif; font-size: 17px;">
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.</p>
<h4 class="" style="box-sizing: border-box; font-family:
'Helvetica Neue', Helvetica, Arial, sans-serif; font-weight:
500; line-height: 1.1; color: rgb(51, 51, 51); margin-top: 10px;
margin-bottom: 10px; font-size: 21px;">
Dates</h4>
<p class="" style="box-sizing: border-box; margin: 0px 0px 10px;
color: rgb(51, 51, 51); font-family: 'Helvetica Neue',
Helvetica, Arial, sans-serif; font-size: 17px;">
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. </p>
<h4 class="" style="box-sizing: border-box; font-family:
'Helvetica Neue', Helvetica, Arial, sans-serif; font-weight:
500; line-height: 1.1; color: rgb(51, 51, 51); margin-top: 10px;
margin-bottom: 10px; font-size: 21px;">
Lecturers and Topics</h4>
<div class="" style="box-sizing: border-box; margin: 0px 0px 10px;
color: rgb(51, 51, 51); font-family: 'Helvetica Neue',
Helvetica, Arial, sans-serif; font-size: 17px;">
<table class="" style="box-sizing: border-box; border-spacing:
0px; border-collapse: collapse; background-color: rgb(255,
255, 224); border: 1px solid black; width: 648px; padding:
15px; color: rgb(51, 51, 51); font-size: 17px;">
<tbody class="" style="box-sizing: border-box;">
<tr class="" style="box-sizing: border-box;">
<td class="" style="box-sizing: border-box; padding: 5px;
border: 1px solid gray;">
Andrew Appel </td>
<td class="" style="box-sizing: border-box; padding: 5px;
border: 1px solid gray;">
Verified functional algorithms </td>
</tr>
<tr class="" style="box-sizing: border-box;">
<td class="" style="box-sizing: border-box; padding: 5px;
border: 1px solid gray;">
Adam Chlipala </td>
<td class="" style="box-sizing: border-box; padding: 5px;
border: 1px solid gray;">
Program-specific proof automation</td>
</tr>
<tr class="" style="box-sizing: border-box;">
<td class="" style="box-sizing: border-box; padding: 5px;
border: 1px solid gray;">
Frans Kaashoek & Nickolai Zeldovich </td>
<td class="" style="box-sizing: border-box; padding: 5px;
border: 1px solid gray;">
Certifying software with crashes </td>
</tr>
<tr class="" style="box-sizing: border-box;">
<td class="" style="box-sizing: border-box; padding: 5px;
border: 1px solid gray; width: 291.23748779296875px;">
Xavier Leroy </td>
<td class="" style="box-sizing: border-box; padding: 5px;
border: 1px solid gray;">
The structure of a verified compiler</td>
</tr>
<tr class="" style="box-sizing: border-box;">
<td class="" style="box-sizing: border-box; padding: 5px;
border: 1px solid gray;">
Benjamin Pierce </td>
<td class="" style="box-sizing: border-box; padding: 5px;
border: 1px solid gray;">
Property-based random testing with QuickChick </td>
</tr>
<tr class="" style="box-sizing: border-box;">
<td class="" style="box-sizing: border-box; padding: 5px;
border: 1px solid gray;">
Zhong Shao </td>
<td class="" style="box-sizing: border-box; padding: 5px;
border: 1px solid gray;">
CertiKOS: Certified kit operating systems</td>
</tr>
<tr class="" style="box-sizing: border-box;">
<td class="" style="box-sizing: border-box; padding: 5px;
border: 1px solid gray;">
Stephanie Weirich </td>
<td class="" style="box-sizing: border-box; padding: 5px;
border: 1px solid gray;">
Language specification and variable binding</td>
</tr>
<tr class="" style="box-sizing: border-box;">
<td class="" style="box-sizing: border-box; padding: 5px;
border: 1px solid gray;">
Steve Zdancewic </td>
<td class="" style="box-sizing: border-box; padding: 5px;
border: 1px solid gray;">
Vellvm: Verifying the LLVM </td>
</tr>
</tbody>
</table>
</div>
<h4 class="" style="box-sizing: border-box; font-family:
'Helvetica Neue', Helvetica, Arial, sans-serif; font-weight:
500; line-height: 1.1; color: rgb(51, 51, 51); margin-top: 10px;
margin-bottom: 10px; font-size: 21px;">
More information</h4>
</div>
<div class=""><span class="" style="color: rgb(51, 51, 51);
font-family: 'Helvetica Neue', Helvetica, Arial, sans-serif;
font-size: 17px; background-color: rgb(255, 255, 255);">To
apply, or for more information, please visit</span><span class="" style="color: rgb(51, 51, 51); font-family: 'Helvetica
Neue', Helvetica, Arial, sans-serif; font-size: 17px;
background-color: rgb(255, 255, 255);"> </span><font class="" face="Helvetica Neue,Helvetica,Arial,sans-serif"><span class="" style="font-size: 17px;"><a href="http://deepspec.org/events/ss17detail.html" class="">http://deepspec.org/events/ss17detail.html</a></span></font>.</div>
<div class=""><span class="" style="color: rgb(51, 51, 51);
font-family: 'Helvetica Neue', Helvetica, Arial, sans-serif;
font-size: 17px; background-color: rgb(255, 255, 255);"><br class="">
</span></div>
<div class=""><span class="" style="color: rgb(51, 51, 51);
font-family: 'Helvetica Neue', Helvetica, Arial, sans-serif;
font-size: 17px; background-color: rgb(255, 255, 255);">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.<br class="">
<br class="">
<font size="-1" class="">Subscribe or unsubscribe from the High
Confidence Software and Systems mailing list here:
<a href="http://cps-vo.org/hcss/mailing" class="">http://cps-vo.org/hcss/mailing</a></font></span></div>
</body></html>