<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:"Cambria Math";
panose-1:2 4 5 3 5 4 6 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:11.0pt;
font-family:"Aptos",sans-serif;
mso-ligatures:standardcontextual;}
span.EmailStyle17
{mso-style-type:personal-compose;
font-family:"Aptos",sans-serif;
color:windowtext;}
.MsoChpDefault
{mso-style-type:export-only;
font-size:11.0pt;}
@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:1322123390;
mso-list-template-ids:456401000;}
@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:1323044078;
mso-list-template-ids:1806831934;}
@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:1610316769;
mso-list-template-ids:1627830850;}
@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:1645088956;
mso-list-template-ids:998691610;}
@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:2050183981;
mso-list-template-ids:1820625574;}
@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"><b>17<sup>th</sup> NASA Formal Methods Symposium (NFM’25)</b><o:p></o:p></p>
<p class="MsoNormal">11-13 June 2025<o:p></o:p></p>
<p class="MsoNormal">Hampton Roads, VA<o:p></o:p></p>
<p class="MsoNormal">Call for Papers<o:p></o:p></p>
<p class="MsoNormal"> <o:p></o:p></p>
<p class="MsoNormal"><b>Symposium Theme </b><o:p></o:p></p>
<p class="MsoNormal">The widespread use and increasing complexity of mission-critical and safety-critical systems at NASA and in the aerospace industry requires advanced technologies to address their specification, design, verification, validation, and certification.
The NASA Formal Methods Symposium is a forum to foster collaboration between theoreticians and practitioners from NASA, other government agencies, academia, and industry, with the goal of identifying challenges and providing solutions towards achieving assurance
for such critical systems. The focus of this symposium is on formal techniques for software and system assurance for applications in space, aviation, robotics, and other NASA-relevant critical systems. <o:p></o:p></p>
<p class="MsoNormal"> <o:p></o:p></p>
<p class="MsoNormal"><b>Topics of Interest </b><o:p></o:p></p>
<ul style="margin-top:0in" type="disc">
<li class="MsoNormal" style="mso-list:l3 level1 lfo1">Advances in Formal Methods – Formal verification, model checking, <br>
and static analysis; interactive and automated theorem proving; program and specification synthesis, code transformation and generation; run-time verification and test case generation; techniques and algorithms for scaling formal methods; design for verification
and correct-by-design techniques; requirements generation, specification, and validation. <o:p></o:p></li></ul>
<ul style="margin-top:0in" type="disc">
<li class="MsoNormal" style="mso-list:l0 level1 lfo2">Integration of Formal Methods – Use of ML techniques in formal methods; integration of formal methods and software engineering; integration of diverse formal methods techniques; integration of formal methods
with simulation, analysis, and test approaches. <o:p></o:p></li></ul>
<ul style="margin-top:0in" type="disc">
<li class="MsoNormal" style="mso-list:l2 level1 lfo3">Formal Methods in Practice – Experience reports on applications of formal methods in industry; use of formal methods in education; applications of formal methods to concurrent and distributed systems, human-machine
systems, autonomous systems, and fault-detection, diagnostics, and prognostics systems. <o:p></o:p></li></ul>
<p class="MsoNormal"> <o:p></o:p></p>
<p class="MsoNormal"><b>Submission </b><o:p></o:p></p>
<p class="MsoNormal">There are two categories of submissions: <o:p></o:p></p>
<ul style="margin-top:0in" type="disc">
<li class="MsoNormal" style="mso-list:l4 level1 lfo4">Regular papers – Up to 15 pages plus references. Regular papers describe fully developed work and complete results. <o:p></o:p></li></ul>
<ul style="margin-top:0in" type="disc">
<li class="MsoNormal" style="mso-list:l1 level1 lfo5">Short papers — Up to 6 pages plus references. Short papers describe either novel and publicly available tools, case studies detailing applications of formal methods, or new emerging ideas in the topics of
interest. <o:p></o:p></li></ul>
<p class="MsoNormal"> <o:p></o:p></p>
<p class="MsoNormal">All papers should be in English and describe original work that has not been published or submitted elsewhere. Authors of accepted papers must present their work in person at the conference. <o:p></o:p></p>
<p class="MsoNormal"> <o:p></o:p></p>
<p class="MsoNormal">NFM prohibits the use of generative AI to create the textual narrative of the paper. However, the use of generative AI to create examples (such as text, tables, graphics, and code) that support the paper is permitted, but this must be disclosed
in the paper. Basic word processing systems that recommend and insert replacement text, perform spelling or grammar checks and corrections, or systems that do language translations need not be disclosed in the paper. <o:p></o:p></p>
<p class="MsoNormal"> <o:p></o:p></p>
<p class="MsoNormal">All submissions will be fully reviewed by at least 3 members of the Program Committee. NFM is currently arranging to publish accepted regular and short papers in the Formal Methods subline of Springer’s Lecture Notes in Computer Science
(LNCS). Authors should therefore use the LNCS style formatting described at<span style="font-family:"Arial",sans-serif"> </span>https://www.springer.com/gp/computer-science/lncs/conference-proceedings-guidelines. Papers must be submitted in PDF format through
the EasyChair submission site,<span style="font-family:"Arial",sans-serif"> </span>https://easychair.org/conferences/?conf=nfm2025. <o:p></o:p></p>
<p class="MsoNormal"> <o:p></o:p></p>
<p class="MsoNormal"><b>Important Dates </b><o:p></o:p></p>
<table class="MsoNormalTable" border="0" cellpadding="0" width="0">
<tbody>
<tr style="height:15.0pt">
<td width="210" valign="top" style="width:157.5pt;padding:0in 0in 0in 0in;height:15.0pt">
<p class="MsoNormal">Paper submission <o:p></o:p></p>
</td>
<td width="203" valign="top" style="width:152.25pt;padding:0in 0in 0in 0in;height:15.0pt">
<p class="MsoNormal">December 13, 2024 <o:p></o:p></p>
</td>
</tr>
<tr style="height:15.0pt">
<td width="210" valign="top" style="width:157.5pt;padding:0in 0in 0in 0in;height:15.0pt">
<p class="MsoNormal">Author notification <o:p></o:p></p>
</td>
<td width="203" valign="top" style="width:152.25pt;padding:0in 0in 0in 0in;height:15.0pt">
<p class="MsoNormal">February 14, 2025 <o:p></o:p></p>
</td>
</tr>
<tr style="height:15.0pt">
<td width="210" valign="top" style="width:157.5pt;padding:0in 0in 0in 0in;height:15.0pt">
<p class="MsoNormal">Camera ready deadline <o:p></o:p></p>
</td>
<td width="203" valign="top" style="width:152.25pt;padding:0in 0in 0in 0in;height:15.0pt">
<p class="MsoNormal">March 14, 2025 <o:p></o:p></p>
</td>
</tr>
<tr style="height:15.0pt">
<td width="210" valign="top" style="width:157.5pt;padding:0in 0in 0in 0in;height:15.0pt">
<p class="MsoNormal">Symposium <o:p></o:p></p>
</td>
<td width="203" valign="top" style="width:152.25pt;padding:0in 0in 0in 0in;height:15.0pt">
<p class="MsoNormal">June 11-13, 2025 <o:p></o:p></p>
</td>
</tr>
</tbody>
</table>
<p class="MsoNormal"> <o:p></o:p></p>
<p class="MsoNormal"><b>Location and Cost </b><o:p></o:p></p>
<p class="MsoNormal">The symposium will take place in Hampton Roads, VA. The exact location is still to be determined. <o:p></o:p></p>
<p class="MsoNormal"> <o:p></o:p></p>
<p class="MsoNormal">There will be no registration fee charged to participants. All interested individuals, including non-US citizens, are welcome to attend, listen to the talks, and participate in discussions. However, all attendees must register. <o:p></o:p></p>
<p class="MsoNormal"> <o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
</body>
</html>