<html xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns="http://www.w3.org/TR/REC-html40">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<meta name="Generator" content="Microsoft Word 15 (filtered medium)">
<style><!--
/* Font Definitions */
@font-face
{font-family:Wingdings;
panose-1:5 0 0 0 0 0 0 0 0 0;}
@font-face
{font-family:"Cambria Math";
panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
{font-family:Calibri;
panose-1:2 15 5 2 2 2 4 3 2 4;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0in;
margin-bottom:.0001pt;
font-size:12.0pt;
font-family:"Calibri",sans-serif;}
a:link, span.MsoHyperlink
{mso-style-priority:99;
color:#0563C1;
text-decoration:underline;}
span.EmailStyle17
{mso-style-type:personal-compose;
font-family:"Calibri",sans-serif;
color:windowtext;}
span.apple-tab-span
{mso-style-name:apple-tab-span;}
.MsoChpDefault
{mso-style-type:export-only;
font-size:12.0pt;
font-family:"Calibri",sans-serif;}
@page WordSection1
{size:8.5in 11.0in;
margin:1.0in 1.0in 1.0in 1.0in;}
div.WordSection1
{page:WordSection1;}
/* List Definitions */
@list l0
{mso-list-id:767429809;
mso-list-template-ids:863654524;}
@list l0:level1
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:.5in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l0:level2
{mso-level-number-format:bullet;
mso-level-text:o;
mso-level-tab-stop:1.0in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:"Courier New";
mso-bidi-font-family:"Times New Roman";}
@list l0:level3
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:1.5in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l0:level4
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:2.0in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l0:level5
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:2.5in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l0:level6
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:3.0in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l0:level7
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:3.5in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l0:level8
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:4.0in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l0:level9
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:4.5in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l1
{mso-list-id:1940523197;
mso-list-template-ids:-651119560;}
@list l1:level1
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:.5in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l1:level2
{mso-level-number-format:bullet;
mso-level-text:o;
mso-level-tab-stop:1.0in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:"Courier New";
mso-bidi-font-family:"Times New Roman";}
@list l1:level3
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:1.5in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l1:level4
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:2.0in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l1:level5
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:2.5in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l1:level6
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:3.0in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l1:level7
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:3.5in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l1:level8
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:4.0in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l1:level9
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:4.5in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
ol
{margin-bottom:0in;}
ul
{margin-bottom:0in;}
--></style>
</head>
<body lang="EN-US" link="#0563C1" vlink="#954F72">
<div class="WordSection1">
<p style="margin:0in;margin-bottom:.0001pt"><span style="font-family:"Arial",sans-serif;color:black">*********************************************************************************</span><o:p></o:p></p>
<p style="margin:0in;margin-bottom:.0001pt"><span style="font-family:"Arial",sans-serif;color:black"> </span><span class="apple-tab-span"><span style="font-family:"Arial",sans-serif;color:black">
</span></span><span style="font-family:"Arial",sans-serif;color:black">The 12th NASA Formal Methods Symposium (NFM2020)</span><o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p style="mso-margin-top-alt:0in;margin-right:0in;margin-bottom:0in;margin-left:.5in;margin-bottom:.0001pt">
<a href="https://ti.arc.nasa.gov/events/nfm-2020/"><span style="font-family:"Arial",sans-serif;color:#1155CC">https://ti.arc.nasa.gov/events/nfm-2020/</span></a><o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p style="margin:0in;margin-bottom:.0001pt"><span class="apple-tab-span"><span style="font-family:"Arial",sans-serif;color:black">
</span></span><span style="font-family:"Arial",sans-serif;color:black">NFM2020 is virtual and organized by the</span><o:p></o:p></p>
<p style="mso-margin-top-alt:0in;margin-right:0in;margin-bottom:0in;margin-left:.5in;margin-bottom:.0001pt">
<span style="font-family:"Arial",sans-serif;color:black">NASA Ames Research Center, Moffett Field, CA, USA</span><o:p></o:p></p>
<p style="mso-margin-top-alt:0in;margin-right:0in;margin-bottom:0in;margin-left:1.0in;margin-bottom:.0001pt;text-indent:.5in">
<span style="font-family:"Arial",sans-serif;color:black">May 11-15, 2020</span><o:p></o:p></p>
<p style="margin:0in;margin-bottom:.0001pt"><span style="font-family:"Arial",sans-serif;color:black">*********************************************************************************</span><o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p style="margin:0in;margin-bottom:.0001pt"><span style="font-family:"Arial",sans-serif;color:black">* There is no registration fee! *</span><o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p style="margin:0in;margin-bottom:.0001pt"><span style="font-family:"Arial",sans-serif;color:black">Virtual Symposium</span><o:p></o:p></p>
<p style="margin:0in;margin-bottom:.0001pt"><span style="font-family:"Arial",sans-serif;color:black">-------------------------</span><o:p></o:p></p>
<p style="margin:0in;margin-bottom:.0001pt"><span style="font-family:"Arial",sans-serif;color:black">Due to concerns about COVID-19, NFM 2020 is going virtual. We invite the formal methods and aligned communities to use this opportunity of a virtual symposium
to participate and engage in a very exciting set of paper presentations and fascinating keynote talks. </span><o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p style="margin:0in;margin-bottom:.0001pt"><span style="font-family:"Arial",sans-serif;color:black">Theme of the Symposium:</span><o:p></o:p></p>
<p style="margin:0in;margin-bottom:.0001pt"><span style="font-family:"Arial",sans-serif;color:black">-----------------------------------</span><o:p></o:p></p>
<p style="margin:0in;margin-bottom:.0001pt"><span style="font-family:"Arial",sans-serif;color:black">The widespread use and increasing complexity of mission-critical and safety-critical systems at NASA and the aerospace industry requires advanced techniques
that address their specification, design, verification, validation, and certification requirements. The NASA Formal Methods Symposium is a forum to foster collaboration between theoreticians and practitioners from NASA, academia, and the industry, with the
goal of identifying challenges and providing solutions towards achieving assurance for such critical systems.</span><o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p style="margin:0in;margin-bottom:.0001pt"><span style="font-family:"Arial",sans-serif;color:black">New developments and emerging applications like autonomous on-board Software for Unmanned Aerial Systems (UAS), UAS Traffic Management (UTM), advanced separation
assurance algorithms for aircraft, and the need for system-wide fault detection, diagnosis, and prognostics provide new challenges for system specification, development, and verification approaches. The focus of these symposiums are on formal techniques and
other approaches for software assurance, including their theory, current capabilities and limitations, as well as their potential application to aerospace, robotics, and other NASA-relevant safety-critical systems during all stages of the software life-cycle.</span><o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p style="margin:0in;margin-bottom:.0001pt"><span style="font-family:"Arial",sans-serif;color:black">The NASA Formal Methods Symposium is an annual event organized by the NASA Formal Methods (NFM) Steering Committee, comprised of researchers spanning several
NASA centers. NFM 2020 is being organized by the NASA Ames Research Center in Moffett Field, CA. More information about past NFM Symposiums can be found here:
</span><a href="https://shemesh.larc.nasa.gov/NFM/"><span style="font-size:10.5pt;font-family:"Arial",sans-serif;color:#1155CC">https://shemesh.larc.nasa.gov/NFM/</span></a><o:p></o:p></p>
<p class="MsoNormal" style="margin-bottom:12.0pt"><o:p> </o:p></p>
<p style="margin:0in;margin-bottom:.0001pt"><span style="font-family:"Arial",sans-serif;color:black">Registration:</span><o:p></o:p></p>
<p style="margin:0in;margin-bottom:.0001pt"><span style="font-family:"Arial",sans-serif;color:black">-----------------</span><o:p></o:p></p>
<p style="margin:0in;margin-bottom:.0001pt"><span style="font-family:"Arial",sans-serif;color:black">There is no registration fee charged to participants. All interested individuals are welcome to attend; however, all attendees must register:
</span><a href="https://ti.arc.nasa.gov/events/nfm-2020/registration/"><span style="font-family:"Arial",sans-serif;color:#1155CC">https://ti.arc.nasa.gov/events/nfm-2020/registration/</span></a><o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p style="margin:0in;margin-bottom:.0001pt"><span style="font-family:"Arial",sans-serif;color:black">Keynote Speakers:</span><o:p></o:p></p>
<p style="margin:0in;margin-bottom:.0001pt"><span style="font-family:"Arial",sans-serif;color:black">-------------------------</span><o:p></o:p></p>
<p style="margin:0in;margin-bottom:.0001pt"><span style="font-family:"Arial",sans-serif;color:black">* Léonard Bouygues (Google Loon)</span><o:p></o:p></p>
<p style="margin:0in;margin-bottom:.0001pt"><span style="font-family:"Arial",sans-serif;color:black">* Byron Cook (Amazon Web Services, University College London)</span><o:p></o:p></p>
<p style="margin:0in;margin-bottom:.0001pt"><span style="font-family:"Arial",sans-serif;color:black">* David Dill (Facebook, Stanford University)</span><o:p></o:p></p>
<p style="margin:0in;margin-bottom:.0001pt"><span style="font-family:"Arial",sans-serif;color:black">* Dana Schulze (National Transportation Safety Board)</span><o:p></o:p></p>
<p style="margin:0in;margin-bottom:.0001pt"><span style="font-family:"Arial",sans-serif;color:black">* Sanjit Seshia (University of California Berkeley)</span><o:p></o:p></p>
<p style="margin:0in;margin-bottom:.0001pt"><span style="font-family:"Arial",sans-serif;color:black">* Vandi Verma (NASA Jet Propulsion Laboratory)</span><o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p style="margin:0in;margin-bottom:.0001pt"><span style="font-family:"Arial",sans-serif;color:black">NFM2020 Program & Workshops</span><o:p></o:p></p>
<p style="margin:0in;margin-bottom:.0001pt"><span style="font-family:"Arial",sans-serif;color:black">--------------------------------------------</span><o:p></o:p></p>
<p style="margin:0in;margin-bottom:.0001pt"><span style="font-family:"Arial",sans-serif;color:black">Please see the program here:
</span><a href="https://ti.arc.nasa.gov/events/nfm-2020/program/"><span style="font-family:"Arial",sans-serif;color:#1155CC">https://ti.arc.nasa.gov/events/nfm-2020/program/</span></a><o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p style="margin:0in;margin-bottom:.0001pt"><span style="font-family:"Arial",sans-serif;color:black">This year there the following two workshops will be virtually hosted with NFM2020:</span><o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p style="margin:0in;margin-bottom:.0001pt"><span style="font-family:"Arial",sans-serif;color:black">* AI Safety Workshop, Monday May 11th, 2020. Confirmed speakers:</span><o:p></o:p></p>
<ul style="margin-top:0in" type="disc">
<li style="color:black;margin-top:0in;margin-bottom:0in;margin-bottom:.0001pt;mso-list:l0 level1 lfo1;vertical-align:baseline">
<span style="font-family:"Arial",sans-serif">Clark Barrett (Stanford University)<o:p></o:p></span></li></ul>
<ul style="margin-top:0in" type="disc">
<li style="color:black;margin-top:0in;margin-bottom:0in;margin-bottom:.0001pt;mso-list:l1 level1 lfo2;vertical-align:baseline">
<span style="font-family:"Arial",sans-serif">Kamalika Chaudhuri (University of California, San Diego)<o:p></o:p></span></li><li style="color:black;margin-top:0in;margin-bottom:0in;margin-bottom:.0001pt;mso-list:l1 level1 lfo2;vertical-align:baseline">
<span style="font-family:"Arial",sans-serif">Krishnamurthy Dvijotham (DeepMind)<o:p></o:p></span></li><li style="color:black;margin-top:0in;margin-bottom:0in;margin-bottom:.0001pt;mso-list:l1 level1 lfo2;vertical-align:baseline">
<span style="font-family:"Arial",sans-serif">Suman Jana (Columbia University)<o:p></o:p></span></li><li style="color:black;margin-top:0in;margin-bottom:0in;margin-bottom:.0001pt;mso-list:l1 level1 lfo2;vertical-align:baseline">
<span style="font-family:"Arial",sans-serif">Nils Jansen (Radboud University Nijmegen)<o:p></o:p></span></li><li style="color:black;margin-top:0in;margin-bottom:0in;margin-bottom:.0001pt;mso-list:l1 level1 lfo2;vertical-align:baseline">
<span style="font-family:"Arial",sans-serif">Mykel Kochenderfer (Stanford University)<o:p></o:p></span></li><li style="color:black;margin-top:0in;margin-bottom:0in;margin-bottom:.0001pt;mso-list:l1 level1 lfo2;vertical-align:baseline">
<span style="font-family:"Arial",sans-serif">Andreas Krause (ETH)<o:p></o:p></span></li><li style="color:black;margin-top:0in;margin-bottom:0in;margin-bottom:.0001pt;mso-list:l1 level1 lfo2;vertical-align:baseline">
<span style="font-family:"Arial",sans-serif">Changliu Liu (Carnegie Mellon University)<o:p></o:p></span></li><li style="color:black;margin-top:0in;margin-bottom:0in;margin-bottom:.0001pt;mso-list:l1 level1 lfo2;vertical-align:baseline">
<span style="font-family:"Arial",sans-serif">James Lopez (GE Research)<o:p></o:p></span></li><li style="color:black;margin-top:0in;margin-bottom:0in;margin-bottom:.0001pt;mso-list:l1 level1 lfo2;vertical-align:baseline">
<span style="font-family:"Arial",sans-serif">Dorsa Sadigh (Stanford University)<o:p></o:p></span></li><li style="color:black;margin-top:0in;margin-bottom:0in;margin-bottom:.0001pt;mso-list:l1 level1 lfo2;vertical-align:baseline">
<span style="font-family:"Arial",sans-serif">Sriram Sankaranarayanan (University of Colorado at Boulder)<o:p></o:p></span></li><li style="color:black;margin-top:0in;margin-bottom:0in;margin-bottom:.0001pt;mso-list:l1 level1 lfo2;vertical-align:baseline">
<span style="font-family:"Arial",sans-serif">Iain Whiteside (Five AI)<o:p></o:p></span></li></ul>
<p style="margin:0in;margin-bottom:.0001pt"><a href="https://sites.google.com/stanford.edu/nfm-ai-safety-20/"><span style="font-family:"Arial",sans-serif;color:#1155CC">https://sites.google.com/stanford.edu/nfm-ai-safety-20/</span></a><o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p style="margin:0in;margin-bottom:.0001pt"><span style="font-family:"Arial",sans-serif;color:black">* Cryptographic Proofs Workshop, Friday 15th 2020</span><o:p></o:p></p>
<p style="margin:0in;margin-bottom:.0001pt"><a href="https://fmcpworkshop.onai.com/"><span style="font-family:"Arial",sans-serif;color:#1155CC">https://fmcpworkshop.onai.com/</span></a><o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p style="margin:0in;margin-bottom:.0001pt"><span style="font-family:"Arial",sans-serif;color:black">Organizers:</span><o:p></o:p></p>
<p style="margin:0in;margin-bottom:.0001pt"><span style="font-family:"Arial",sans-serif;color:black">---------------</span><o:p></o:p></p>
<p style="margin:0in;margin-bottom:.0001pt"><span style="font-family:"Arial",sans-serif;color:black">* Dimitra Giannakopoulou (General co-Chair)</span><o:p></o:p></p>
<p style="margin:0in;margin-bottom:.0001pt"><span style="font-family:"Arial",sans-serif;color:black">* Anastasia Mavridou (General co-Chair)</span><o:p></o:p></p>
<p style="margin:0in;margin-bottom:.0001pt"><span style="font-family:"Arial",sans-serif;color:black">* Ritchie Lee (PC co-Chair)</span><o:p></o:p></p>
<p style="margin:0in;margin-bottom:.0001pt"><span style="font-family:"Arial",sans-serif;color:black">* Susmit Jha (PC co-Chair)</span><o:p></o:p></p>
<p style="margin:0in;margin-bottom:.0001pt"><span style="font-family:"Arial",sans-serif;color:black">* Hamza Bourbouh (Local Organization)</span><o:p></o:p></p>
<p style="margin:0in;margin-bottom:.0001pt"><span style="font-family:"Arial",sans-serif;color:black">* Maxime Arthaud (Local Organization)</span><o:p></o:p></p>
<p class="MsoNormal" style="margin-bottom:12.0pt"><br>
<br>
<br>
<o:p></o:p></p>
<p class="MsoNormal"><span style="font-size:11.0pt"><o:p> </o:p></span></p>
</div>
</body>
</html>