<html xmlns:v="urn:schemas-microsoft-com:vml" 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)">
<!--[if !mso]><style>v\:* {behavior:url(#default#VML);}
o\:* {behavior:url(#default#VML);}
w\:* {behavior:url(#default#VML);}
.shape {behavior:url(#default#VML);}
</style><![endif]--><style><!--
/* Font Definitions */
@font-face
{font-family:Helvetica;
panose-1:0 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;}
@font-face
{font-family:"Calibri Light";
panose-1:2 15 3 2 2 2 4 3 2 4;}
@font-face
{font-family:Aptos;
panose-1:2 11 0 4 2 2 2 2 2 4;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0in;
font-size:12.0pt;
font-family:"Aptos",sans-serif;
mso-ligatures:standardcontextual;}
a:link, span.MsoHyperlink
{mso-style-priority:99;
color:#467886;
text-decoration:underline;}
span.EmailStyle17
{mso-style-type:personal-compose;
font-family:"Aptos",sans-serif;
color:windowtext;}
span.apple-converted-space
{mso-style-name:apple-converted-space;}
.MsoChpDefault
{mso-style-type:export-only;}
@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:27995845;
mso-list-template-ids:-741550150;}
@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:;
mso-level-tab-stop:1.0in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@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:Symbol;}
@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:Symbol;}
@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:Symbol;}
@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:Symbol;}
@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:Symbol;}
@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:Symbol;}
@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:Symbol;}
@list l1
{mso-list-id:942417377;
mso-list-template-ids:-1234141664;}
@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:;
mso-level-tab-stop:1.0in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@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:Symbol;}
@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:Symbol;}
@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:Symbol;}
@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:Symbol;}
@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:Symbol;}
@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:Symbol;}
@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:Symbol;}
@list l2
{mso-list-id:1028413994;
mso-list-template-ids:-1504559906;}
@list l2: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 l2:level2
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:1.0in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l2: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:Symbol;}
@list l2: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:Symbol;}
@list l2: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:Symbol;}
@list l2: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:Symbol;}
@list l2: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:Symbol;}
@list l2: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:Symbol;}
@list l2: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:Symbol;}
@list l3
{mso-list-id:1811239490;
mso-list-template-ids:-565259172;}
@list l3: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 l3:level2
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:1.0in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l3: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:Symbol;}
@list l3: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:Symbol;}
@list l3: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:Symbol;}
@list l3: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:Symbol;}
@list l3: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:Symbol;}
@list l3: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:Symbol;}
@list l3: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:Symbol;}
@list l4
{mso-list-id:1943806624;
mso-list-template-ids:1003795658;}
@list l4: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 l4:level2
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:1.0in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l4: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:Symbol;}
@list l4: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:Symbol;}
@list l4: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:Symbol;}
@list l4: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:Symbol;}
@list l4: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:Symbol;}
@list l4: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:Symbol;}
@list l4: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:Symbol;}
ol
{margin-bottom:0in;}
ul
{margin-bottom:0in;}
--></style>
</head>
<body lang="EN-US" link="#467886" vlink="#96607D" style="word-wrap:break-word">
<div class="WordSection1">
<p class="MsoNormal"><span style="font-size:13.5pt;color:black">-----------------------------------------<o:p></o:p></span></p>
<p class="MsoNormal" style="font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;caret-color: rgb(0, 0, 0);word-spacing:0px">
<span style="font-size:13.5pt;color:black">Call for Participation: NFM 2025<o:p></o:p></span></p>
<p class="MsoNormal" style="font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;caret-color: rgb(0, 0, 0);word-spacing:0px">
<span style="font-size:13.5pt;color:black">-----------------------------------------<o:p></o:p></span></p>
<p class="MsoNormal" style="font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;caret-color: rgb(0, 0, 0);word-spacing:0px">
<span style="font-size:13.5pt;color:black"> <o:p></o:p></span></p>
<p class="MsoNormal" style="font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;caret-color: rgb(0, 0, 0);word-spacing:0px">
<b><span style="font-size:13.5pt;color:black">The 17th NASA Formal Methods Symposium</span></b><span style="font-size:13.5pt;color:black"><o:p></o:p></span></p>
<p class="MsoNormal" style="font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;caret-color: rgb(0, 0, 0);word-spacing:0px">
<span style="font-size:13.5pt;color:black">----------------<o:p></o:p></span></p>
<p class="MsoNormal" style="font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;caret-color: rgb(0, 0, 0);word-spacing:0px">
<span style="font-size:13.5pt;color:black">30 Years of Formal Methods at NASA<o:p></o:p></span></p>
<p class="MsoNormal" style="font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;caret-color: rgb(0, 0, 0);word-spacing:0px">
<span style="font-size:13.5pt;color:black">June 11-13, Williamsburg, Virginia, United States of America<o:p></o:p></span></p>
<p class="MsoNormal" style="font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;caret-color: rgb(0, 0, 0);word-spacing:0px">
<span style="font-size:13.5pt;color:black"><a href="https://shemesh.larc.nasa.gov/nfm2025/" title="https://shemesh.larc.nasa.gov/nfm2025/"><span style="color:#467886">https://shemesh.larc.nasa.gov/nfm2025/</span></a> <<a href="https://shemesh.larc.nasa.gov/nfm2025/" title="https://shemesh.larc.nasa.gov/nfm2025/"><span style="color:#467886">https://shemesh.larc.nasa.gov/nfm2025/</span></a>><o:p></o:p></span></p>
<p class="MsoNormal" style="caret-color: rgb(0, 0, 0);font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;word-spacing:0px">
<span style="font-size:13.5pt;color:black"> <o:p></o:p></span></p>
<p class="MsoNormal" style="font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;caret-color: rgb(0, 0, 0);word-spacing:0px">
<b><span style="font-size:13.5pt;color:black">Keynote speakers</span></b><span style="font-size:13.5pt;color:black"><o:p></o:p></span></p>
<p class="MsoNormal" style="font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;caret-color: rgb(0, 0, 0);word-spacing:0px">
<span style="font-size:13.5pt;color:black">----------------<o:p></o:p></span></p>
<p class="MsoNormal" style="font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;caret-color: rgb(0, 0, 0);word-spacing:0px">
<span style="font-size:13.5pt;color:black">Darren Cofer (Collins Aerospace)<o:p></o:p></span></p>
<p class="MsoNormal" style="font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;caret-color: rgb(0, 0, 0);word-spacing:0px">
<span style="font-size:13.5pt;color:black">Emina Torlak (Amazon Web Services)<o:p></o:p></span></p>
<p class="MsoNormal" style="font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;caret-color: rgb(0, 0, 0);word-spacing:0px">
<span style="font-size:13.5pt;color:black">Natasha Neogi and Paul Miner (NASA)<o:p></o:p></span></p>
<p class="MsoNormal" style="font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;caret-color: rgb(0, 0, 0);word-spacing:0px">
<span style="font-size:13.5pt;color:black"> <o:p></o:p></span></p>
<p class="MsoNormal" style="font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;caret-color: rgb(0, 0, 0);word-spacing:0px">
<span style="font-size:13.5pt;color:black">The program of symposium is available at:<o:p></o:p></span></p>
<p class="MsoNormal" style="font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;caret-color: rgb(0, 0, 0);word-spacing:0px">
<span style="font-size:13.5pt;color:black"><a href="https://shemesh.larc.nasa.gov/nfm2025/program.html" title="https://shemesh.larc.nasa.gov/nfm2025/program.html"><span style="color:#467886">https://shemesh.larc.nasa.gov/nfm2025/program.html</span></a> <<a href="https://shemesh.larc.nasa.gov/nfm2025/program.html" title="https://shemesh.larc.nasa.gov/nfm2025/program.html"><span style="color:#467886">https://shemesh.larc.nasa.gov/nfm2025/program.html</span></a>><o:p></o:p></span></p>
<p class="MsoNormal" style="font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;caret-color: rgb(0, 0, 0);word-spacing:0px">
<span style="font-size:13.5pt;color:black"> <o:p></o:p></span></p>
<p class="MsoNormal" style="font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;caret-color: rgb(0, 0, 0);word-spacing:0px">
<span style="font-size:13.5pt;color:black">Attendance to the symposium is free, but all attendees must register in order to participate.<o:p></o:p></span></p>
<p class="MsoNormal" style="font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;caret-color: rgb(0, 0, 0);word-spacing:0px">
<span style="font-size:13.5pt;color:black">Registrations is open at:<o:p></o:p></span></p>
<p class="MsoNormal" style="font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;caret-color: rgb(0, 0, 0);word-spacing:0px">
<span style="font-size:13.5pt;color:black"><a href="https://shemesh.larc.nasa.gov/nfm2025/registration.html" title="https://shemesh.larc.nasa.gov/nfm2025/registration.html"><span style="color:#467886">https://shemesh.larc.nasa.gov/nfm2025/registration.html</span></a> <<a href="https://shemesh.larc.nasa.gov/nfm2025/registration.html" title="https://shemesh.larc.nasa.gov/nfm2025/registration.html"><span style="color:#467886">https://shemesh.larc.nasa.gov/nfm2025/registration.html</span></a>><o:p></o:p></span></p>
<p class="MsoNormal" style="font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;caret-color: rgb(0, 0, 0);word-spacing:0px">
<span style="font-size:13.5pt;color:black"> <o:p></o:p></span></p>
<p class="MsoNormal" style="font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;caret-color: rgb(0, 0, 0);word-spacing:0px">
<span style="font-size:13.5pt;color:black">The symposium will be held at the College of William and Mary at<o:p></o:p></span></p>
<p class="MsoNormal" style="font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;caret-color: rgb(0, 0, 0);word-spacing:0px">
<span style="font-size:13.5pt;color:black"> <o:p></o:p></span></p>
<p class="MsoNormal" style="font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;caret-color: rgb(0, 0, 0);word-spacing:0px">
<span style="font-size:13.5pt;color:black">Sadler Center<o:p></o:p></span></p>
<p class="MsoNormal" style="font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;caret-color: rgb(0, 0, 0);word-spacing:0px">
<span style="font-size:13.5pt;color:black">200 Stadium Drive<o:p></o:p></span></p>
<p class="MsoNormal" style="font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;caret-color: rgb(0, 0, 0);word-spacing:0px">
<span style="font-size:13.5pt;color:black">Williamsburg, VA 23186<o:p></o:p></span></p>
<p class="MsoNormal" style="font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;caret-color: rgb(0, 0, 0);word-spacing:0px">
<span style="font-size:13.5pt;color:black">For more information about travel and lodging options, see<span class="apple-converted-space"> </span></span><u><span style="font-size:13.5pt;color:blue"><a href="https://shemesh.larc.nasa.gov/nfm2025/venue.html" title="https://shemesh.larc.nasa.gov/nfm2025/venue.html"><span style="color:#467886">https://shemesh.larc.nasa.gov/nfm2025/venue.html</span></a></span></u><span style="font-size:13.5pt;color:black"> <<a href="https://shemesh.larc.nasa.gov/nfm2025/venue.html" title="https://shemesh.larc.nasa.gov/nfm2025/venue.html"><span style="color:#467886">https://shemesh.larc.nasa.gov/nfm2025/venue.html</span></a>><o:p></o:p></span></p>
<p class="MsoNormal" style="caret-color: rgb(0, 0, 0);font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;word-spacing:0px">
<span style="font-size:13.5pt;color:black"> <o:p></o:p></span></p>
<p class="MsoNormal" style="font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;caret-color: rgb(0, 0, 0);word-spacing:0px">
<b><span style="font-size:13.5pt;color:black">List of Accepted Papers</span></b><span style="font-size:13.5pt;color:black"><o:p></o:p></span></p>
<p class="MsoNormal" style="font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;caret-color: rgb(0, 0, 0);word-spacing:0px">
<span style="font-size:13.5pt;color:black">----------------<o:p></o:p></span></p>
<p class="MsoNormal" style="font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;caret-color: rgb(0, 0, 0);word-spacing:0px">
<span style="font-size:13.5pt;color:black"> <o:p></o:p></span></p>
<ul style="margin-top:0in;font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;caret-color: rgb(0, 0, 0);word-spacing:0px" type="disc">
<li class="MsoNormal" style="color:black;mso-list:l1 level1 lfo1">Arthur Amorim, Max Taylor, Trevor Kann, William Harrison, Gary Leavens, and Lance Joneckis. <i>Enforcing MAVLink Safety & Security Properties Via Refined Multiparty Session Types</i><o:p></o:p></li><li class="MsoNormal" style="color:black;mso-list:l1 level1 lfo1">Ziggy Attala, Fang Yan, Simon Foster, Ana Cavalcanti, and Jim Woodcock. <i>Process-Algebraic Semantics for Verifying Intelligent Robotic Control Software</i><o:p></o:p></li><li class="MsoNormal" style="color:black;mso-list:l1 level1 lfo1">Alexis Aurandt, Phillip Jones, and Kristin Yvonne Rozier. <i>Towards a Safe, Verified Runtime Monitor for Embedded Systems: R2U2 in Embedded Rust</i><o:p></o:p></li><li class="MsoNormal" style="color:black;mso-list:l1 level1 lfo1">Mauricio Ayala-Rincón, Thaynara Arielly de Lima, Maria Júlia Dias Lima, Mariano Moscato, and Temur Kutsia. <i>Verification of an Anti-Unification Algorithm in PVS</i><o:p></o:p></li><li class="MsoNormal" style="color:black;mso-list:l1 level1 lfo1">Max Bannach, Jai Grover, and Markus Hecher. <i>Strong Structural Bounds for MaxSAT: The Fine Details of Using Neuromorphic and Quantum Hardware Accelerators</i><o:p></o:p></li><li class="MsoNormal" style="color:black;mso-list:l1 level1 lfo1">Calvin Beck, Hanxi Chen, and Steve Zdancewic. <i>Vellvm: Formalizing the Informal LLVM (Experience Report)</i><o:p></o:p></li><li class="MsoNormal" style="color:black;mso-list:l1 level1 lfo1">Andrea Bombarda, Silvia Bonfanti, Angelo Gargantini, and Nico Pellegrinelli. <i>Eliminating Flakiness: Deterministic Control for Validating Nondeterministic Asmeta Specifications</i><o:p></o:p></li><li class="MsoNormal" style="color:black;mso-list:l1 level1 lfo1">Matías Brizzio, Felipe Gorostiaga, Cesar Sanchez, and Renzo Degiovanni. <i>Mode-based Reactive Synthesis</i><o:p></o:p></li><li class="MsoNormal" style="color:black;mso-list:l1 level1 lfo1">Pranav Ghorpade, Nathalie Bertrand, Sasha Rubin, Bernhard Scholz, and Pavle Subotic. <i>Reusable Formal Verification of DAG-based Consensus Protocols</i><o:p></o:p></li><li class="MsoNormal" style="color:black;mso-list:l1 level1 lfo1">Andreas Katis, Anastasia Mavridou, and Thomas Pressburger. <i>A Streamlined, Formal Approach to Requirements-based Testing</i><o:p></o:p></li><li class="MsoNormal" style="color:black;mso-list:l1 level1 lfo1">Elias Khalife, Pierre-Loic Garoche, and Mazen Farhood. <i>Formally Proving Invariant Systemic Properties of Control Programs Using Ghost Code and Integral Quadratic Constraints</i><o:p></o:p></li><li class="MsoNormal" style="color:black;mso-list:l1 level1 lfo1">Edward Kim, Devan Shanker, Varun Bharadwaj, Hongbeen Park, Jinkyu Kim, Hazem Torfah, Daniel Fremont, and Sanjit Seshia. <i>Querying Labeled Time Series Data with Scenario Programs</i><o:p></o:p></li><li class="MsoNormal" style="color:black;mso-list:l1 level1 lfo1">Ignacio D. Lopez-Miguel, Borja Fernández Adiego, Matias Salinas, and Christine Betz. <i>Formal Verification as a Service: A CERN-GSI Case Study</i><o:p></o:p></li><li class="MsoNormal" style="color:black;mso-list:l1 level1 lfo1">Sumio Morioka, Satoshi Obana, and Maki Yoshida. <i>Formal Verification of Composite Field Multipliers for Information-Theoretically Secure Radio Communication in Spacecraft Control</i><o:p></o:p></li><li class="MsoNormal" style="color:black;mso-list:l1 level1 lfo1">Mathis Niehage, Carina da Silva, Anne Remke, and Arnd Hartmanns. <i>Rare Event Simulation for Stochastic Hybrid Systems using Symbolic Importance Functions</i><o:p></o:p></li><li class="MsoNormal" style="color:black;mso-list:l1 level1 lfo1">Carlos Olarte, Daniel Osorio, Carlos Ramirez, and Camilo Rocha. <i>Algorithmic Analysis of Event-B in Rewriting Logic</i><o:p></o:p></li><li class="MsoNormal" style="color:black;mso-list:l1 level1 lfo1">Jainta Paul, Stefan Mitsch, and Luis Garcia. <i>HyTwin: A Formal Semantics for Digital Twin Interventions in ICS Based on Time-to-Violation</i><o:p></o:p></li><li class="MsoNormal" style="color:black;mso-list:l1 level1 lfo1">Alec Rosentrater, Zili Wang, Katherine Kosaian, and Kristin Yvonne Rozier. <i>Language Partitioning for Mission-time Linear Temporal Logic</i><o:p></o:p></li><li class="MsoNormal" style="color:black;mso-list:l1 level1 lfo1">Nafiz Sadman, Nastaran Kianersi, and Sean Kauffman. <i>Visualizing Temporal Interval Hierarchies</i><o:p></o:p></li><li class="MsoNormal" style="color:black;mso-list:l1 level1 lfo1">Mohit Tekriwal and Matthew Sottile. <i>Mechanized RS274 semantics for additive manufacturing</i><o:p></o:p></li><li class="MsoNormal" style="color:black;mso-list:l1 level1 lfo1">Benjamin Valpey, Xinyi Li, Sreepathi Pai, and Ganesh Gopalakrishnan. <i>An SMT Formalization of Mixed-Precision Matrix Multiplication (Modeling Three Generations of Tensor Cores)</i><o:p></o:p></li><li class="MsoNormal" style="color:black;mso-list:l1 level1 lfo1">Sarat Chandra Varanasi, Baoluo Meng, Robert Lorch, Abha Moitra, Kit Siu, Saswata Paul, Michael During, Neha Beniwal, and Nikita Visnevski. <i>TRACE: Toolkit for Requirements Analysis, Capture,
and Elicitation</i><o:p></o:p></li><li class="MsoNormal" style="color:black;mso-list:l1 level1 lfo1">Jian Xiang and Stephen Chong. <i>Extending Dynamic Logics with First-Class Relational Reasoning</i><o:p></o:p></li><li class="MsoNormal" style="color:black;mso-list:l1 level1 lfo1">Michal Šedý and Lukáš Holík. <i>Automata Size Reduction by Procedure Finding</i><o:p></o:p></li></ul>
<p class="MsoNormal" style="font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;caret-color: rgb(0, 0, 0);word-spacing:0px">
<span style="font-size:13.5pt;color:black"> <o:p></o:p></span></p>
<p class="MsoNormal" style="font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;caret-color: rgb(0, 0, 0);word-spacing:0px">
<b><span style="font-size:13.5pt;color:black">Organizing Committee</span></b><span style="font-size:13.5pt;color:black"><o:p></o:p></span></p>
<p class="MsoNormal" style="font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;caret-color: rgb(0, 0, 0);word-spacing:0px">
<span style="font-size:13.5pt;color:black">----------------<o:p></o:p></span></p>
<p class="MsoNormal" style="font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;caret-color: rgb(0, 0, 0);word-spacing:0px">
<span style="font-size:13.5pt;color:black">Conference Chair<o:p></o:p></span></p>
<ul style="margin-top:0in;font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;caret-color: rgb(0, 0, 0);word-spacing:0px" type="disc">
<li class="MsoNormal" style="color:black;mso-list:l3 level1 lfo2"><a href="https://gcc02.safelinks.protection.outlook.com/?url=https%3A%2F%2Flauratitolo.github.io%2F&data=05%7C02%7Cfm-announcements%40lists.nasa.gov%7Cd5c3f43085604eea92a308dd88a9216a%7C7005d45845be48ae8140d43da96dd17b%7C0%7C0%7C638816982162717205%7CUnknown%7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ%3D%3D%7C0%7C%7C%7C&sdata=Kc4G6O11ylNhkTN53LXW8T%2FaStUhDSE6XTVYuY4G36c%3D&reserved=0" originalsrc="https://lauratitolo.github.io/" title="https://lauratitolo.github.io/"><span style="color:#467886">Laura
Titolo</span></a> (CodeMetal)<o:p></o:p></li></ul>
<p class="MsoNormal" style="font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;caret-color: rgb(0, 0, 0);word-spacing:0px">
<span style="font-size:13.5pt;color:black">Program Committee Chairs<o:p></o:p></span></p>
<ul style="margin-top:0in;font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;caret-color: rgb(0, 0, 0);word-spacing:0px" type="disc">
<li class="MsoNormal" style="color:black;mso-list:l0 level1 lfo3"><a href="https://shemesh.larc.nasa.gov/people/amd" title="https://shemesh.larc.nasa.gov/people/amd"><span style="color:#467886">Aaron Dutle</span></a> (NASA)<o:p></o:p></li><li class="MsoNormal" style="color:black;mso-list:l0 level1 lfo3">Laura Humphrey (NASA)<o:p></o:p></li></ul>
<p class="MsoNormal" style="font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;caret-color: rgb(0, 0, 0);word-spacing:0px">
<span style="font-size:13.5pt;color:black">Local Organization<o:p></o:p></span></p>
<ul style="margin-top:0in;font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;caret-color: rgb(0, 0, 0);word-spacing:0px" type="disc">
<li class="MsoNormal" style="color:black;mso-list:l4 level1 lfo4"><a href="https://gcc02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fwww.wm.edu%2Fas%2Fcomputerscience%2Fpeople%2Fsun_yifan.php&data=05%7C02%7Cfm-announcements%40lists.nasa.gov%7Cd5c3f43085604eea92a308dd88a9216a%7C7005d45845be48ae8140d43da96dd17b%7C0%7C0%7C638816982162738647%7CUnknown%7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ%3D%3D%7C0%7C%7C%7C&sdata=EFGB%2BJ%2BSsfpn6574pVzWhBRaAAbXzDvvIXmcR3aN%2Bss%3D&reserved=0" originalsrc="https://www.wm.edu/as/computerscience/people/sun_yifan.php" title="https://www.wm.edu/as/computerscience/people/sun_yifan.php"><span style="color:#467886">Yifan
Sun</span></a> (William & Mary)<o:p></o:p></li><li class="MsoNormal" style="color:black;mso-list:l4 level1 lfo4"><a href="https://gcc02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fmarianomoscato.github.io%2F&data=05%7C02%7Cfm-announcements%40lists.nasa.gov%7Cd5c3f43085604eea92a308dd88a9216a%7C7005d45845be48ae8140d43da96dd17b%7C0%7C0%7C638816982162754852%7CUnknown%7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ%3D%3D%7C0%7C%7C%7C&sdata=%2BMMx6%2FHwWTNi%2FEScRUl2yYPXVTYpXijkfjuCaUuCVlM%3D&reserved=0" originalsrc="https://marianomoscato.github.io/" title="https://marianomoscato.github.io/"><span style="color:#467886">Mariano
Moscato</span></a> (AMA Inc.)<o:p></o:p></li></ul>
<p class="MsoNormal" style="font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;caret-color: rgb(0, 0, 0);word-spacing:0px">
<span style="font-size:13.5pt;color:black">Publicity<o:p></o:p></span></p>
<ul style="margin-top:0in;font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;caret-color: rgb(0, 0, 0);word-spacing:0px" type="disc">
<li class="MsoNormal" style="color:black;mso-list:l2 level1 lfo5"><a href="https://shemesh.larc.nasa.gov/people/jts" title="https://shemesh.larc.nasa.gov/people/jts"><span style="color:#467886">J Tanner Slagel</span></a> (NASA)<o:p></o:p></li></ul>
<p class="MsoNormal" style="font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;caret-color: rgb(0, 0, 0);word-spacing:0px">
<span style="font-size:13.5pt;color:black"> <o:p></o:p></span></p>
<p class="MsoNormal" style="font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;caret-color: rgb(0, 0, 0);word-spacing:0px">
<span style="font-size:13.5pt;color:black">Contact<o:p></o:p></span></p>
<p class="MsoNormal" style="font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;caret-color: rgb(0, 0, 0);word-spacing:0px">
<span style="font-size:13.5pt;color:black">--------<o:p></o:p></span></p>
<p class="MsoNormal" style="font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;caret-color: rgb(0, 0, 0);word-spacing:0px">
<span style="font-size:13.5pt;color:black">Email: nfm2025 [at] easychair [dot] org<o:p></o:p></span></p>
<p class="MsoNormal" style="font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;caret-color: rgb(0, 0, 0);word-spacing:0px">
<span style="font-size:13.5pt;color:black">Web: <a href="https://shemesh.larc.nasa.gov/nfm2025/index.html#loc-home" title="https://shemesh.larc.nasa.gov/nfm2025/index.html#loc-home"><span style="color:#467886">https://shemesh.larc.nasa.gov/nfm2025/index.html
- loc-home</span></a> <<a href="https://shemesh.larc.nasa.gov/nfm2025/index.html#loc-home" title="https://shemesh.larc.nasa.gov/nfm2025/index.html#loc-home"><span style="color:#467886">https://shemesh.larc.nasa.gov/nfm2025/index.html - loc-home</span></a>><o:p></o:p></span></p>
<p class="MsoNormal" style="font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;caret-color: rgb(0, 0, 0);word-spacing:0px">
<span style="font-size:13.5pt;color:black"> <o:p></o:p></span></p>
<p class="MsoNormal" style="font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;caret-color: rgb(0, 0, 0);word-spacing:0px">
<span style="font-size:13.5pt;color:black">Sincerely,<o:p></o:p></span></p>
<p class="MsoNormal" style="font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;caret-color: rgb(0, 0, 0);word-spacing:0px">
<span style="font-size:13.5pt;color:black">Tanner<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt"><o:p> </o:p></span></p>
<div>
<table class="MsoNormalTable" border="0" cellspacing="0" cellpadding="0" width="540" style="width:405.0pt;border-collapse:collapse">
<tbody>
<tr style="height:91.3pt">
<td width="121" style="width:90.85pt;padding:2.15pt 1.45pt 2.15pt 1.45pt;height:91.3pt">
<p class="MsoNormal" align="center" style="text-align:center"><a href="https://www.nasa.gov/" title="https://www.nasa.gov/"><span style="font-size:11.0pt;font-family:"Calibri Light",sans-serif;color:black;text-decoration:none"><img border="0" width="115" height="115" style="width:1.1979in;height:1.1979in" id="Picture_x0020_2" src="cid:image001.png@01DBBA70.778CC7E0" alt="NASA Meatball Logo"></span></a><span style="font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ligatures:none"><o:p></o:p></span></p>
</td>
<td width="29" valign="bottom" style="width:21.65pt;padding:2.15pt 1.45pt 2.15pt 1.45pt;height:91.3pt">
<p class="MsoNormal" align="center" style="text-align:center;line-height:12.65pt">
<span style="font-size:11.0pt;font-family:"Calibri Light",sans-serif;mso-ligatures:none"><img border="0" width="2" height="145" style="width:.0208in;height:1.5104in" id="Picture_x0020_1" src="cid:image002.png@01DBBA70.778CC7E0" alt="cid76989*image005.png@01DB789B.48F08D70"></span><span style="font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ligatures:none"><o:p></o:p></span></p>
</td>
<td width="390" style="width:292.5pt;padding:2.15pt 1.45pt 2.15pt 1.45pt;height:91.3pt">
<p class="MsoNormal" style="line-height:12.65pt"><b><span style="font-size:11.0pt;font-family:Helvetica;color:black;mso-ligatures:none">J Tanner Slagel</span></b><span style="font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ligatures:none"><o:p></o:p></span></p>
<p class="MsoNormal" style="line-height:12.65pt"><b><span style="font-size:9.0pt;font-family:Helvetica;color:black;mso-ligatures:none">Research Computer Scientist
<o:p></o:p></span></b></p>
<p class="MsoNormal" style="line-height:12.65pt"><span style="font-size:9.0pt;color:black;mso-ligatures:none">Safety Critical Avionics Systems Branch<o:p></o:p></span></p>
<p class="MsoNormal" style="line-height:12.65pt"><span style="font-size:9.0pt;color:black;mso-ligatures:none">NASA Langley Research Center</span><span style="font-size:9.0pt;font-family:Helvetica;color:black;mso-ligatures:none"><o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:9.0pt;font-family:Helvetica;mso-ligatures:none"><a href="mailto:j.tanner.slagel@nasa.gov"><span style="color:#467886">j.tanner.slagel@nasa.gov</span></a></span><span style="font-size:11.0pt;font-family:"Calibri",sans-serif;mso-ligatures:none"><o:p></o:p></span></p>
</td>
</tr>
</tbody>
</table>
</div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
</body>
</html>