<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:Calibri;
panose-1:2 15 5 2 2 2 4 3 2 4;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0in;
font-size:12.0pt;
font-family:"Calibri",sans-serif;
mso-ligatures:standardcontextual;}
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;}
.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;}
--></style>
</head>
<body lang="EN-US" link="#0563C1" vlink="#954F72" style="word-wrap:break-word">
<div class="WordSection1">
<p class="MsoNormal"><span style="font-size:11.0pt">The NASA Formal Methods community invites you to submit a paper to:<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">The 16th NASA Formal Methods Symposium (NFM 2024)<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">June 4-6, 2024<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">Moffett Field, California<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"><a href="https://conf.researchr.org/home/nfm-2024">https://conf.researchr.org/home/nfm-2024</a><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>
<p class="MsoNormal"><span style="font-size:11.0pt">Important Dates:<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>
<p class="MsoNormal"><span style="font-size:11.0pt">Abstract submission: December 1, 2023<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">Full paper submission: December 8, 2023<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">Notification: February 16, 2024<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">Camera-ready version: March 15, 2024<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>
<p class="MsoNormal"><span style="font-size:11.0pt">Theme of the Symposium:<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>
<p class="MsoNormal"><span style="font-size:11.0pt">The widespread use and increasing complexity of mission-critical and
<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">safety-critical systems at NASA and in the aerospace industry requires advanced<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">technologies to address their specification, design, verification, validation,
<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">and certification processes. For example, there is an increasing need for
<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">autonomous systems in deep space missions including NASA’s Moon to Mars
<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">exploration plans. The NASA Formal Methods Symposium is a forum to foster
<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">collaboration between theoreticians and practitioners from NASA, other
<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">government agencies, academia, and industry, with the goal of identifying
<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">challenges and providing solutions towards achieving assurance for such
<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">critical systems. The focus of this symposium is on formal techniques for
<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">software and system assurance for applications in space, aviation, robotics,
<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">and other NASA-relevant safety-critical systems. This year’s symposium extends
<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">the focus to safety assurance of machine learning enabled autonomous systems,<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">formal methods for digital transformation, and accessibility for new
<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">industries.<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>
<p class="MsoNormal"><span style="font-size:11.0pt">Topics of Interest:<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>
<p class="MsoNormal"><span style="font-size:11.0pt">Advances in Formal Methods <o:p>
</o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">* Formal verification, model checking, and static analysis
<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">* Interactive and automated theorem proving
<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">* Program and specification synthesis, code transformation and generation
<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">* Run-time verification and test case generation
<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">* Techniques and algorithms for scaling formal methods
<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">* Design for verification and correct-by-design techniques
<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">* Requirements generation, specification, and validation
<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">Integration of Formal Methods<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">* Use of machine learning techniques in formal methods<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">* Integration of formal methods and software engineering<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">* Integration of diverse formal methods techniques<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">* Combination of formal methods with simulation and analysis techniques<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">Formal Methods in Practice<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">* Experience reports of application of formal methods in industry<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">* Use of formal methods in education<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">* Applications of formal methods in:<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt"> - concurrent and distributed systems<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt"> - fault-detection, diagnostics, and prognostics systems<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt"> - human-machine interaction analysis<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">Safety Assurance of Autonomous Systems<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">* Verification of machine learning (ML) enabled systems<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">* Runtime monitoring or model checking to ensure safe operation<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">* Formal specifications and modeling of ML enabled systems<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">* Case-studies/experience reports exploring the application of formal methods
<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt"> in autonomous safety-critical, cyber-physical and hybrid systems<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">* Using formal evidence for certification of ML enabled systems<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">Formal Methods for Digital Transformation<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">* Applications related to Digital Twin & Digital Thread<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">* Verification for integrated design and manufacturing<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">* AI digital assistants for system design<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">* Runtime monitoring for Smart Campus & Smart Cities<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">Accessibility of Formal Methods for New Industries<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">* "New Space" markets <o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">* Advanced Air Mobility and Startup Aviation<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">* Formal Methods as a Service<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>
<p class="MsoNormal"><span style="font-size:11.0pt">Submissions:<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>
<p class="MsoNormal"><span style="font-size:11.0pt">There are two categories of submissions:<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">* Regular Papers (15 pages including references), describing fully developed
<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt"> work and complete results<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">* Short Papers (6 pages including references), in one of the categories below:
<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt"> - Tool papers describing novel and publicly available tools<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt"> - Case studies detailing applications of formal methods<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt"> - New emerging ideas in the topics of interest<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">All papers should be in English and describe original work that has not been
<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">published or submitted elsewhere. NFM24 will be a hybrid conference. Authors of<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">accepted papers are encouraged to present their work in person at the
<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">conference. <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">There will be a tool demonstration session at the conference, where tool
<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">developers get to showcase their tools interactively with the attendees. All
<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">tool papers, under the short papers category, are required to participate in
<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">the tool demonstration session. Authors of regular papers are also welcome to
<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">participate in the tool demonstration session to showcase their application.
<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">All submitters who are interested in participating in the tool demonstration
<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">session must include an additional appendix (maximum 4 pages and will not
<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">appear in the proceedings) containing the description of the proposed demo and
<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">the URL to a screencast demonstrating the tool. Authors of all accepted papers
<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">additionally have an opportunity to present a poster.
<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">All submissions will be fully reviewed by members of the Program Committee.
<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">Accepted regular and short papers will be published in the Formal Methods
<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">subline of Springer’s Lecture Notes in Computer Science (LNCS) and must use
<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">LNCS style formatting described on
<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt"><a href="https://www.springer.com/gp/computer-science/lncs/conference-proceedings-guidelines">https://www.springer.com/gp/computer-science/lncs/conference-proceedings-guidelines</a>.
<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">Papers must be submitted in PDF format at the EasyChair submission site,
<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt"><a href="https://easychair.org/conferences/?conf=nfm2024">https://easychair.org/conferences/?conf=nfm2024</a>.<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>
<p class="MsoNormal"><span style="font-size:11.0pt">Location and Cost:<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>
<p class="MsoNormal"><span style="font-size:11.0pt">The symposium will take place at the NASA Ames Conference Center,<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">Moffett Field, California, USA.<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">There will be no registration fee charged to participants. All<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">interested individuals, including non-US citizens, are welcome to<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">attend, listen to the talks, and participate in discussions. However,<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">all attendees must register.<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>
<p class="MsoNormal"><span style="font-size:11.0pt">Nathan Benz<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">Divya Gopinath<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">Nija Shi<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">NFM '24 Chairs<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt"><a href="mailto:nfm24-chairs@lists.nasa.gov">nfm24-chairs@lists.nasa.gov</a><o:p></o:p></span></p>
</div>
</body>
</html>