<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;}
a:visited, span.MsoHyperlinkFollowed
        {mso-style-priority:99;
        color:#954F72;
        text-decoration:underline;}
span.EmailStyle17
        {mso-style-type:personal-compose;
        font-family:"Calibri",sans-serif;
        color:windowtext;}
span.apple-converted-space
        {mso-style-name:apple-converted-space;}
.MsoChpDefault
        {mso-style-type:export-only;
        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:354893660;
        mso-list-type:hybrid;
        mso-list-template-ids:-1954619084 67698693 67698691 67698693 67698689 67698691 67698693 67698689 67698691 67698693;}
@list l0:level1
        {mso-level-number-format:bullet;
        mso-level-text:;
        mso-level-tab-stop:none;
        mso-level-number-position:left;
        margin-left:77.0pt;
        text-indent:-.25in;
        font-family:Wingdings;}
@list l0:level2
        {mso-level-number-format:bullet;
        mso-level-text:o;
        mso-level-tab-stop:none;
        mso-level-number-position:left;
        margin-left:113.0pt;
        text-indent:-.25in;
        font-family:"Courier New";}
@list l0:level3
        {mso-level-number-format:bullet;
        mso-level-text:;
        mso-level-tab-stop:none;
        mso-level-number-position:left;
        margin-left:149.0pt;
        text-indent:-.25in;
        font-family:Wingdings;}
@list l0:level4
        {mso-level-number-format:bullet;
        mso-level-text:;
        mso-level-tab-stop:none;
        mso-level-number-position:left;
        margin-left:185.0pt;
        text-indent:-.25in;
        font-family:Symbol;}
@list l0:level5
        {mso-level-number-format:bullet;
        mso-level-text:o;
        mso-level-tab-stop:none;
        mso-level-number-position:left;
        margin-left:221.0pt;
        text-indent:-.25in;
        font-family:"Courier New";}
@list l0:level6
        {mso-level-number-format:bullet;
        mso-level-text:;
        mso-level-tab-stop:none;
        mso-level-number-position:left;
        margin-left:257.0pt;
        text-indent:-.25in;
        font-family:Wingdings;}
@list l0:level7
        {mso-level-number-format:bullet;
        mso-level-text:;
        mso-level-tab-stop:none;
        mso-level-number-position:left;
        margin-left:293.0pt;
        text-indent:-.25in;
        font-family:Symbol;}
@list l0:level8
        {mso-level-number-format:bullet;
        mso-level-text:o;
        mso-level-tab-stop:none;
        mso-level-number-position:left;
        margin-left:329.0pt;
        text-indent:-.25in;
        font-family:"Courier New";}
@list l0:level9
        {mso-level-number-format:bullet;
        mso-level-text:;
        mso-level-tab-stop:none;
        mso-level-number-position:left;
        margin-left:365.0pt;
        text-indent:-.25in;
        font-family:Wingdings;}
@list l1
        {mso-list-id:1236743674;
        mso-list-type:hybrid;
        mso-list-template-ids:219567656 67698689 67698691 67698693 67698689 67698691 67698693 67698689 67698691 67698693;}
@list l1:level1
        {mso-level-number-format:bullet;
        mso-level-text:;
        mso-level-tab-stop:none;
        mso-level-number-position:left;
        text-indent:-.25in;
        font-family:Symbol;}
@list l1:level2
        {mso-level-number-format:bullet;
        mso-level-text:o;
        mso-level-tab-stop:none;
        mso-level-number-position:left;
        text-indent:-.25in;
        font-family:"Courier New";}
@list l1:level3
        {mso-level-number-format:bullet;
        mso-level-text:;
        mso-level-tab-stop:none;
        mso-level-number-position:left;
        text-indent:-.25in;
        font-family:Wingdings;}
@list l1:level4
        {mso-level-number-format:bullet;
        mso-level-text:;
        mso-level-tab-stop:none;
        mso-level-number-position:left;
        text-indent:-.25in;
        font-family:Symbol;}
@list l1:level5
        {mso-level-number-format:bullet;
        mso-level-text:o;
        mso-level-tab-stop:none;
        mso-level-number-position:left;
        text-indent:-.25in;
        font-family:"Courier New";}
@list l1:level6
        {mso-level-number-format:bullet;
        mso-level-text:;
        mso-level-tab-stop:none;
        mso-level-number-position:left;
        text-indent:-.25in;
        font-family:Wingdings;}
@list l1:level7
        {mso-level-number-format:bullet;
        mso-level-text:;
        mso-level-tab-stop:none;
        mso-level-number-position:left;
        text-indent:-.25in;
        font-family:Symbol;}
@list l1:level8
        {mso-level-number-format:bullet;
        mso-level-text:o;
        mso-level-tab-stop:none;
        mso-level-number-position:left;
        text-indent:-.25in;
        font-family:"Courier New";}
@list l1:level9
        {mso-level-number-format:bullet;
        mso-level-text:;
        mso-level-tab-stop:none;
        mso-level-number-position:left;
        text-indent:-.25in;
        font-family:Wingdings;}
@list l2
        {mso-list-id:1307784805;
        mso-list-type:hybrid;
        mso-list-template-ids:-501727554 1218190318 1583793860 67698693 67698689 67698691 67698693 67698689 67698691 67698693;}
@list l2:level1
        {mso-level-start-at:0;
        mso-level-number-format:bullet;
        mso-level-text:·;
        mso-level-tab-stop:none;
        mso-level-number-position:left;
        margin-left:59.0pt;
        text-indent:-.25in;
        mso-ansi-font-size:10.0pt;
        font-family:"Calibri",sans-serif;
        mso-fareast-font-family:"Times New Roman";}
@list l2:level2
        {mso-level-start-at:0;
        mso-level-number-format:bullet;
        mso-level-text:;
        mso-level-tab-stop:none;
        mso-level-number-position:left;
        margin-left:95.0pt;
        text-indent:-.25in;
        mso-ansi-font-size:10.0pt;
        font-family:Symbol;
        mso-fareast-font-family:"Times New Roman";
        mso-bidi-font-family:"Courier New";}
@list l2:level3
        {mso-level-number-format:bullet;
        mso-level-text:;
        mso-level-tab-stop:none;
        mso-level-number-position:left;
        margin-left:131.0pt;
        text-indent:-.25in;
        font-family:Wingdings;}
@list l2:level4
        {mso-level-number-format:bullet;
        mso-level-text:;
        mso-level-tab-stop:none;
        mso-level-number-position:left;
        margin-left:167.0pt;
        text-indent:-.25in;
        font-family:Symbol;}
@list l2:level5
        {mso-level-number-format:bullet;
        mso-level-text:o;
        mso-level-tab-stop:none;
        mso-level-number-position:left;
        margin-left:203.0pt;
        text-indent:-.25in;
        font-family:"Courier New";}
@list l2:level6
        {mso-level-number-format:bullet;
        mso-level-text:;
        mso-level-tab-stop:none;
        mso-level-number-position:left;
        margin-left:239.0pt;
        text-indent:-.25in;
        font-family:Wingdings;}
@list l2:level7
        {mso-level-number-format:bullet;
        mso-level-text:;
        mso-level-tab-stop:none;
        mso-level-number-position:left;
        margin-left:275.0pt;
        text-indent:-.25in;
        font-family:Symbol;}
@list l2:level8
        {mso-level-number-format:bullet;
        mso-level-text:o;
        mso-level-tab-stop:none;
        mso-level-number-position:left;
        margin-left:311.0pt;
        text-indent:-.25in;
        font-family:"Courier New";}
@list l2:level9
        {mso-level-number-format:bullet;
        mso-level-text:;
        mso-level-tab-stop:none;
        mso-level-number-position:left;
        margin-left:347.0pt;
        text-indent:-.25in;
        font-family:Wingdings;}
@list l3
        {mso-list-id:1856579287;
        mso-list-type:hybrid;
        mso-list-template-ids:-1628147020 1218190318 67698691 67698693 67698689 67698691 67698693 67698689 67698691 67698693;}
@list l3:level1
        {mso-level-start-at:0;
        mso-level-number-format:bullet;
        mso-level-text:·;
        mso-level-tab-stop:none;
        mso-level-number-position:left;
        margin-left:59.0pt;
        text-indent:-.25in;
        mso-ansi-font-size:10.0pt;
        font-family:"Calibri",sans-serif;
        mso-fareast-font-family:"Times New Roman";}
@list l3:level2
        {mso-level-number-format:bullet;
        mso-level-text:o;
        mso-level-tab-stop:none;
        mso-level-number-position:left;
        text-indent:-.25in;
        font-family:"Courier New";}
@list l3:level3
        {mso-level-number-format:bullet;
        mso-level-text:;
        mso-level-tab-stop:none;
        mso-level-number-position:left;
        text-indent:-.25in;
        font-family:Wingdings;}
@list l3:level4
        {mso-level-number-format:bullet;
        mso-level-text:;
        mso-level-tab-stop:none;
        mso-level-number-position:left;
        text-indent:-.25in;
        font-family:Symbol;}
@list l3:level5
        {mso-level-number-format:bullet;
        mso-level-text:o;
        mso-level-tab-stop:none;
        mso-level-number-position:left;
        text-indent:-.25in;
        font-family:"Courier New";}
@list l3:level6
        {mso-level-number-format:bullet;
        mso-level-text:;
        mso-level-tab-stop:none;
        mso-level-number-position:left;
        text-indent:-.25in;
        font-family:Wingdings;}
@list l3:level7
        {mso-level-number-format:bullet;
        mso-level-text:;
        mso-level-tab-stop:none;
        mso-level-number-position:left;
        text-indent:-.25in;
        font-family:Symbol;}
@list l3:level8
        {mso-level-number-format:bullet;
        mso-level-text:o;
        mso-level-tab-stop:none;
        mso-level-number-position:left;
        text-indent:-.25in;
        font-family:"Courier New";}
@list l3:level9
        {mso-level-number-format:bullet;
        mso-level-text:;
        mso-level-tab-stop:none;
        mso-level-number-position:left;
        text-indent:-.25in;
        font-family:Wingdings;}
@list l4
        {mso-list-id:2051109793;
        mso-list-type:hybrid;
        mso-list-template-ids:1674231420 1218190318 67698691 67698693 67698689 67698691 67698693 67698689 67698691 67698693;}
@list l4:level1
        {mso-level-start-at:0;
        mso-level-number-format:bullet;
        mso-level-text:·;
        mso-level-tab-stop:none;
        mso-level-number-position:left;
        margin-left:59.0pt;
        text-indent:-.25in;
        mso-ansi-font-size:10.0pt;
        font-family:"Calibri",sans-serif;
        mso-fareast-font-family:"Times New Roman";}
@list l4:level2
        {mso-level-number-format:bullet;
        mso-level-text:o;
        mso-level-tab-stop:none;
        mso-level-number-position:left;
        text-indent:-.25in;
        font-family:"Courier New";}
@list l4:level3
        {mso-level-number-format:bullet;
        mso-level-text:;
        mso-level-tab-stop:none;
        mso-level-number-position:left;
        text-indent:-.25in;
        font-family:Wingdings;}
@list l4:level4
        {mso-level-number-format:bullet;
        mso-level-text:;
        mso-level-tab-stop:none;
        mso-level-number-position:left;
        text-indent:-.25in;
        font-family:Symbol;}
@list l4:level5
        {mso-level-number-format:bullet;
        mso-level-text:o;
        mso-level-tab-stop:none;
        mso-level-number-position:left;
        text-indent:-.25in;
        font-family:"Courier New";}
@list l4:level6
        {mso-level-number-format:bullet;
        mso-level-text:;
        mso-level-tab-stop:none;
        mso-level-number-position:left;
        text-indent:-.25in;
        font-family:Wingdings;}
@list l4:level7
        {mso-level-number-format:bullet;
        mso-level-text:;
        mso-level-tab-stop:none;
        mso-level-number-position:left;
        text-indent:-.25in;
        font-family:Symbol;}
@list l4:level8
        {mso-level-number-format:bullet;
        mso-level-text:o;
        mso-level-tab-stop:none;
        mso-level-number-position:left;
        text-indent:-.25in;
        font-family:"Courier New";}
@list l4:level9
        {mso-level-number-format:bullet;
        mso-level-text:;
        mso-level-tab-stop:none;
        mso-level-number-position:left;
        text-indent:-.25in;
        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;background:white"><span style="color:black">****************************************************<o:p></o:p></span></p>
<p style="margin:0in;margin-bottom:.0001pt;background:white;caret-color: rgb(0, 0, 0);font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-size-adjust: auto;-webkit-text-stroke-width: 0px;background-position:initial initial;background-repeat:initial initial;word-spacing:0px">
<span style="color:black">     The Twelfth NASA Formal Methods Symposium     <o:p></o:p></span></p>
<p style="margin:0in;margin-bottom:.0001pt;text-indent:.5in;background:white;caret-color: rgb(0, 0, 0);font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-size-adjust: auto;-webkit-text-stroke-width: 0px;background-position:initial initial;background-repeat:initial initial;word-spacing:0px">
<span style="color:black"> <a href="https://ti.arc.nasa.gov/events/nfm-2020/"><span style="color:#1155CC">https://ti.arc.nasa.gov/events/nfm-2020/</span></a><o:p></o:p></span></p>
<p style="margin:0in;margin-bottom:.0001pt;background:white;caret-color: rgb(0, 0, 0);font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-size-adjust: auto;-webkit-text-stroke-width: 0px;background-position:initial initial;background-repeat:initial initial;word-spacing:0px">
<span style="color:black">                   11 - 15 May 2020                   <o:p></o:p></span></p>
<p style="margin:0in;margin-bottom:.0001pt;background:white;caret-color: rgb(0, 0, 0);font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-size-adjust: auto;-webkit-text-stroke-width: 0px;background-position:initial initial;background-repeat:initial initial;word-spacing:0px">
<span style="color:black">        NASA Ames Research Center, Moffett Field, CA, USA<o:p></o:p></span></p>
<p style="margin:0in;margin-bottom:.0001pt;background:white;caret-color: rgb(0, 0, 0);font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-size-adjust: auto;-webkit-text-stroke-width: 0px;background-position:initial initial;background-repeat:initial initial;word-spacing:0px">
<span style="color:black">****************************************************<o:p></o:p></span></p>
<p style="margin:0in;margin-bottom:.0001pt;background:white"><span style="color:black"><o:p> </o:p></span></p>
<p style="margin:0in;margin-bottom:.0001pt;background:white;caret-color: rgb(0, 0, 0);font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-size-adjust: auto;-webkit-text-stroke-width: 0px;background-position:initial initial;background-repeat:initial initial;word-spacing:0px">
<span style="color:black">Theme of the Symposium:<o:p></o:p></span></p>
<p style="margin:0in;margin-bottom:.0001pt;background:white;caret-color: rgb(0, 0, 0);font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-size-adjust: auto;-webkit-text-stroke-width: 0px;background-position:initial initial;background-repeat:initial initial;word-spacing:0px">
<span style="color:black">-----------------------<o:p></o:p></span></p>
<p style="margin:0in;margin-bottom:.0001pt;background:white;caret-color: rgb(0, 0, 0);font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-size-adjust: auto;-webkit-text-stroke-width: 0px;background-position:initial initial;background-repeat:initial initial;word-spacing:0px">
<span style="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 industry, with the goal of identifying challenges and providing solutions towards achieving assurance for such
 critical systems. 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.<o:p></o:p></span></p>
<p style="margin:0in;margin-bottom:.0001pt;background:white"><span style="color:black"> <o:p></o:p></span></p>
<p style="margin:0in;margin-bottom:.0001pt;background:white;caret-color: rgb(0, 0, 0);font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-size-adjust: auto;-webkit-text-stroke-width: 0px;background-position:initial initial;background-repeat:initial initial;word-spacing:0px">
<span style="color:black">Topics of Interest:<o:p></o:p></span></p>
<p style="margin:0in;margin-bottom:.0001pt;background:white;caret-color: rgb(0, 0, 0);font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-size-adjust: auto;-webkit-text-stroke-width: 0px;background-position:initial initial;background-repeat:initial initial;word-spacing:0px">
<span style="color:black">-------------------<o:p></o:p></span></p>
<p style="margin-bottom:11.0pt;background:white;caret-color: rgb(0, 0, 0);font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-size-adjust: auto;-webkit-text-stroke-width: 0px;background-position:initial initial;background-repeat:initial initial;word-spacing:0px">
<span style="color:black">We encourage submissions on cross-cutting approaches that bring together formal methods and techniques from other domains such as probabilistic reasoning, machine learning, control theory, robotics, and quantum computing among others.<o:p></o:p></span></p>
<ul type="square">
<li style="color:black;margin-right:11.0pt;margin-bottom:0in;margin-left:41.0pt;margin-bottom:.0001pt;mso-list:l0 level1 lfo5;background:white;vertical-align:baseline">
Formal verification, including theorem proving, model checking, and static analysis<o:p></o:p></li><li style="color:black;margin-right:11.0pt;margin-bottom:0in;margin-left:41.0pt;margin-bottom:.0001pt;mso-list:l0 level1 lfo5;background:white;vertical-align:baseline">
Advances in automated theorem proving including SAT and SMT solving<o:p></o:p></li><li style="color:black;margin-right:11.0pt;margin-bottom:0in;margin-left:41.0pt;margin-bottom:.0001pt;mso-list:l0 level1 lfo5;background:white;vertical-align:baseline">
Run-time verification<o:p></o:p></li><li style="color:black;margin-right:11.0pt;margin-bottom:0in;margin-left:41.0pt;margin-bottom:.0001pt;mso-list:l0 level1 lfo5;background:white;vertical-align:baseline">
Techniques and algorithms for scaling formal methods, such as abstraction and symbolic methods, compositional techniques, as well as parallel and/or distributed techniques<o:p></o:p></li><li style="color:black;margin-right:11.0pt;margin-bottom:0in;margin-left:41.0pt;margin-bottom:.0001pt;mso-list:l0 level1 lfo5;background:white;vertical-align:baseline">
Code generation from formally verified models<o:p></o:p></li><li style="color:black;margin-right:11.0pt;margin-bottom:0in;margin-left:41.0pt;margin-bottom:.0001pt;mso-list:l0 level1 lfo5;background:white;vertical-align:baseline">
Safety cases and system safety<o:p></o:p></li><li style="color:black;margin-right:11.0pt;margin-bottom:0in;margin-left:41.0pt;margin-bottom:.0001pt;mso-list:l0 level1 lfo5;background:white;vertical-align:baseline">
Formal approaches to fault tolerance<o:p></o:p></li><li style="color:black;margin-right:11.0pt;margin-bottom:0in;margin-left:41.0pt;margin-bottom:.0001pt;mso-list:l0 level1 lfo5;background:white;vertical-align:baseline">
Design for verification and correct-by-design techniques<o:p></o:p></li><li style="color:black;margin-right:11.0pt;margin-bottom:0in;margin-left:41.0pt;margin-bottom:.0001pt;mso-list:l0 level1 lfo5;background:white;vertical-align:baseline">
Theoretical advances and empirical evaluations of formal methods techniques for safety-critical systems, including hybrid and embedded systems<o:p></o:p></li><li style="color:black;margin-right:11.0pt;margin-bottom:0in;margin-left:41.0pt;margin-bottom:.0001pt;mso-list:l0 level1 lfo5;background:white;vertical-align:baseline">
Formal methods in systems engineering and model-based development<o:p></o:p></li><li style="color:black;margin-right:11.0pt;margin-bottom:0in;margin-left:41.0pt;margin-bottom:.0001pt;mso-list:l0 level1 lfo5;background:white;vertical-align:baseline">
Applications of formal methods in the development of:<o:p></o:p></li><ul type="circle">
<li style="color:black;margin-right:22.0pt;margin-bottom:0in;margin-left:41.0pt;margin-bottom:.0001pt;mso-list:l0 level2 lfo5;background:white;vertical-align:baseline">
autonomous systems<o:p></o:p></li><li style="color:black;margin-right:22.0pt;margin-bottom:0in;margin-left:41.0pt;margin-bottom:.0001pt;mso-list:l0 level2 lfo5;background:white;vertical-align:baseline">
safety-critical artificial intelligence systems<o:p></o:p></li><li style="color:black;margin-right:22.0pt;margin-bottom:0in;margin-left:41.0pt;margin-bottom:.0001pt;mso-list:l0 level2 lfo5;background:white;vertical-align:baseline">
cyber-physical, cyber-security, embedded, and hybrid systems<o:p></o:p></li><li style="color:black;margin-right:22.0pt;margin-bottom:0in;margin-left:41.0pt;margin-bottom:.0001pt;mso-list:l0 level2 lfo5;background:white;vertical-align:baseline">
fault-detection, diagnostics, and prognostics systems<o:p></o:p></li></ul>
<li style="color:black;margin-right:11.0pt;margin-bottom:0in;margin-left:41.0pt;margin-bottom:.0001pt;mso-list:l0 level1 lfo5;background:white;vertical-align:baseline">
Use of formal methods in:<o:p></o:p></li><ul type="circle">
<li style="color:black;margin-right:22.0pt;margin-bottom:0in;margin-left:41.0pt;margin-bottom:.0001pt;mso-list:l0 level2 lfo5;background:white;vertical-align:baseline">
assurance cases<o:p></o:p></li><li style="color:black;margin-right:22.0pt;margin-bottom:0in;margin-left:41.0pt;margin-bottom:.0001pt;mso-list:l0 level2 lfo5;background:white;vertical-align:baseline">
human-machine interaction analysis<o:p></o:p></li><li style="color:black;margin-right:22.0pt;margin-bottom:0in;margin-left:41.0pt;margin-bottom:.0001pt;mso-list:l0 level2 lfo5;background:white;vertical-align:baseline">
requirements generation, specification, and validation<o:p></o:p></li><li style="color:black;margin-right:22.0pt;margin-bottom:44.0pt;margin-left:41.0pt;mso-list:l0 level2 lfo5;background:white;vertical-align:baseline">
automated testing and verification<o:p></o:p></li></ul>
</ul>
<p style="margin:0in;margin-bottom:.0001pt;background:white;caret-color: rgb(0, 0, 0);font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-size-adjust: auto;-webkit-text-stroke-width: 0px;background-position:initial initial;background-repeat:initial initial;word-spacing:0px">
<span style="color:black">Important Dates:<o:p></o:p></span></p>
<p style="margin:0in;margin-bottom:.0001pt;background:white;caret-color: rgb(0, 0, 0);font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-size-adjust: auto;-webkit-text-stroke-width: 0px;background-position:initial initial;background-repeat:initial initial;word-spacing:0px">
<span style="color:black">----------------<o:p></o:p></span></p>
<p style="margin:0in;margin-bottom:.0001pt;background:white;caret-color: rgb(0, 0, 0);font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-size-adjust: auto;-webkit-text-stroke-width: 0px;background-position:initial initial;background-repeat:initial initial;word-spacing:0px">
<span style="color:black">Abstract Submission:  12 Dec 2019<o:p></o:p></span></p>
<p style="margin:0in;margin-bottom:.0001pt;background:white;caret-color: rgb(0, 0, 0);font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-size-adjust: auto;-webkit-text-stroke-width: 0px;background-position:initial initial;background-repeat:initial initial;word-spacing:0px">
<span style="color:black">Paper Submission:    19 Dec 2019<o:p></o:p></span></p>
<p style="margin:0in;margin-bottom:.0001pt;background:white;caret-color: rgb(0, 0, 0);font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-size-adjust: auto;-webkit-text-stroke-width: 0px;background-position:initial initial;background-repeat:initial initial;word-spacing:0px">
<span style="color:black">Paper Notifications: 20 Feb 2020<o:p></o:p></span></p>
<p style="margin:0in;margin-bottom:.0001pt;background:white;caret-color: rgb(0, 0, 0);font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-size-adjust: auto;-webkit-text-stroke-width: 0px;background-position:initial initial;background-repeat:initial initial;word-spacing:0px">
<span style="color:black">Camera-ready Papers: 27 Mar 2020<o:p></o:p></span></p>
<p style="margin:0in;margin-bottom:.0001pt;background:white;caret-color: rgb(0, 0, 0);font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-size-adjust: auto;-webkit-text-stroke-width: 0px;background-position:initial initial;background-repeat:initial initial;word-spacing:0px">
<span style="color:black">Symposium:          11-15 May 2020<o:p></o:p></span></p>
<p style="margin:0in;margin-bottom:.0001pt;background:white;caret-color: rgb(0, 0, 0);font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-size-adjust: auto;-webkit-text-stroke-width: 0px;background-position:initial initial;background-repeat:initial initial;word-spacing:0px">
<span style="color:black"> <o:p></o:p></span></p>
<p style="margin:0in;margin-bottom:.0001pt;background:white;caret-color: rgb(0, 0, 0);font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-size-adjust: auto;-webkit-text-stroke-width: 0px;background-position:initial initial;background-repeat:initial initial;word-spacing:0px">
<span style="color:black">Location & Cost:<o:p></o:p></span></p>
<p style="margin:0in;margin-bottom:.0001pt;background:white;caret-color: rgb(0, 0, 0);font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-size-adjust: auto;-webkit-text-stroke-width: 0px;background-position:initial initial;background-repeat:initial initial;word-spacing:0px">
<span style="color:black">----------------<o:p></o:p></span></p>
<p style="margin:0in;margin-bottom:.0001pt;background:white;caret-color: rgb(0, 0, 0);font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-size-adjust: auto;-webkit-text-stroke-width: 0px;background-position:initial initial;background-repeat:initial initial;word-spacing:0px">
<span style="color:black">The symposium will take place in Building 3, NASA Ames Research Center, Moffett Field, CA,USA, May 11--15, 2020.<o:p></o:p></span></p>
<p style="margin:0in;margin-bottom:.0001pt;background:white;caret-color: rgb(0, 0, 0);font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-size-adjust: auto;-webkit-text-stroke-width: 0px;background-position:initial initial;background-repeat:initial initial;word-spacing:0px">
<span style="color:black">There will be no registration fee for participants. All interested individuals, including non-US citizens, are welcome to attend, to listen to the talks, and to participate in discussions; however, all attendees must register.<o:p></o:p></span></p>
<p style="margin:0in;margin-bottom:.0001pt;background:white;caret-color: rgb(0, 0, 0);font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-size-adjust: auto;-webkit-text-stroke-width: 0px;background-position:initial initial;background-repeat:initial initial;word-spacing:0px">
<span style="color:black"> <o:p></o:p></span></p>
<p style="margin:0in;margin-bottom:.0001pt;background:white;caret-color: rgb(0, 0, 0);font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-size-adjust: auto;-webkit-text-stroke-width: 0px;background-position:initial initial;background-repeat:initial initial;word-spacing:0px">
<span style="color:black">Organizers:<o:p></o:p></span></p>
<p style="margin:0in;margin-bottom:.0001pt;background:white;caret-color: rgb(0, 0, 0);font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-size-adjust: auto;-webkit-text-stroke-width: 0px;background-position:initial initial;background-repeat:initial initial;word-spacing:0px">
<span style="color:black">-----------<o:p></o:p></span></p>
<p style="margin:0in;margin-bottom:.0001pt;background:white;caret-color: rgb(0, 0, 0);font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-size-adjust: auto;-webkit-text-stroke-width: 0px;background-position:initial initial;background-repeat:initial initial;word-spacing:0px">
<span style="color:black">Dimitra Giannakopoulou (General Chair)<o:p></o:p></span></p>
<p style="margin:0in;margin-bottom:.0001pt;background:white;caret-color: rgb(0, 0, 0);font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-size-adjust: auto;-webkit-text-stroke-width: 0px;background-position:initial initial;background-repeat:initial initial;word-spacing:0px">
<span style="color:black">Anastasia Mavridou (General Chair)<o:p></o:p></span></p>
<p style="margin:0in;margin-bottom:.0001pt;background:white;caret-color: rgb(0, 0, 0);font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-size-adjust: auto;-webkit-text-stroke-width: 0px;background-position:initial initial;background-repeat:initial initial;word-spacing:0px">
<span style="color:black">Ritchie<span class="apple-converted-space"> </span>Lee (PC Chair)<o:p></o:p></span></p>
<p style="margin:0in;margin-bottom:.0001pt;background:white;caret-color: rgb(0, 0, 0);font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-size-adjust: auto;-webkit-text-stroke-width: 0px;background-position:initial initial;background-repeat:initial initial;word-spacing:0px">
<span style="color:black">Susmit Jha (PC Chair)<o:p></o:p></span></p>
<p style="margin:0in;margin-bottom:.0001pt;background:white;caret-color: rgb(0, 0, 0);font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-size-adjust: auto;-webkit-text-stroke-width: 0px;background-position:initial initial;background-repeat:initial initial;word-spacing:0px">
<span style="color:black">Maxime Arthaud (Local Organization)<o:p></o:p></span></p>
<p style="margin:0in;margin-bottom:.0001pt;background:white"><span style="color:black">Hamza Bourbouh (Local Organization)<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt"><o:p> </o:p></span></p>
</div>
</body>
</html>