<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=Windows-1252">
<style type="text/css" style="display:none;"> P {margin-top:0;margin-bottom:0;} </style>
</head>
<body dir="ltr">
<div style="font-family: Aptos, Aptos_EmbeddedFont, Aptos_MSFontService, Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);" class="elementToProof ContentPasted0">
The NASA Formal Methods community invites you to submit a paper to:
<div><br class="ContentPasted0">
</div>
<div class="ContentPasted0">The 16th NASA Formal Methods Symposium (NFM 2024)</div>
<div><br class="ContentPasted0">
</div>
<div class="ContentPasted0">June 4-6, 2024</div>
<div class="ContentPasted0">Moffett Field, California</div>
<div><br class="ContentPasted0">
</div>
<div class="ContentPasted0">https://conf.researchr.org/home/nfm-2024</div>
<div><br class="ContentPasted0">
</div>
<div class="ContentPasted0">--------------------------------------------------</div>
<div class="ContentPasted0">Important Dates:</div>
<div class="ContentPasted0">--------------------------------------------------</div>
<div><br class="ContentPasted0">
</div>
<div class="ContentPasted0">Abstract submission: December 1, 2023</div>
<div class="ContentPasted0">Full paper submission: December 8, 2023</div>
<div class="ContentPasted0">Notification: February 16, 2024</div>
<div class="ContentPasted0">Camera-ready version: March 15, 2024</div>
<div><br class="ContentPasted0">
</div>
<div class="ContentPasted0">--------------------------------------------------</div>
<div class="ContentPasted0">Theme of the Symposium:</div>
<div class="ContentPasted0">--------------------------------------------------</div>
<div><br class="ContentPasted0">
</div>
<div class="ContentPasted0">The widespread use and increasing complexity of mission-critical and
</div>
<div class="ContentPasted0">safety-critical systems at NASA and in the aerospace industry requires advanced</div>
<div class="ContentPasted0">technologies to address their specification, design, verification, validation,
</div>
<div class="ContentPasted0">and certification processes. For example, there is an increasing need for
</div>
<div class="ContentPasted0">autonomous systems in deep space missions including NASA’s Moon to Mars
</div>
<div class="ContentPasted0">exploration plans. The NASA Formal Methods Symposium is a forum to foster
</div>
<div class="ContentPasted0">collaboration between theoreticians and practitioners from NASA, other
</div>
<div class="ContentPasted0">government agencies, academia, and industry, with the goal of identifying
</div>
<div class="ContentPasted0">challenges and providing solutions towards achieving assurance for such
</div>
<div class="ContentPasted0">critical systems. The focus of this symposium is on formal techniques for
</div>
<div class="ContentPasted0">software and system assurance for applications in space, aviation, robotics,
</div>
<div class="ContentPasted0">and other NASA-relevant safety-critical systems. This year’s symposium extends
</div>
<div class="ContentPasted0">the focus to safety assurance of machine learning enabled autonomous systems,</div>
<div class="ContentPasted0">formal methods for digital transformation, and accessibility for new
</div>
<div class="ContentPasted0">industries.</div>
<div><br class="ContentPasted0">
</div>
<div class="ContentPasted0">--------------------------------------------------</div>
<div class="ContentPasted0">Topics of Interest:</div>
<div class="ContentPasted0">--------------------------------------------------</div>
<div><br class="ContentPasted0">
</div>
<div class="ContentPasted0">Advances in Formal Methods </div>
<div class="ContentPasted0">* Formal verification, model checking, and static analysis
</div>
<div class="ContentPasted0">* Interactive and automated theorem proving </div>
<div class="ContentPasted0">* Program and specification synthesis, code transformation and generation
</div>
<div class="ContentPasted0">* Run-time verification and test case generation </div>
<div class="ContentPasted0">* Techniques and algorithms for scaling formal methods
</div>
<div class="ContentPasted0">* Design for verification and correct-by-design techniques
</div>
<div class="ContentPasted0">* Requirements generation, specification, and validation
</div>
<div><br class="ContentPasted0">
</div>
<div class="ContentPasted0">Integration of Formal Methods</div>
<div class="ContentPasted0">* Use of machine learning techniques in formal methods</div>
<div class="ContentPasted0">* Integration of formal methods and software engineering</div>
<div class="ContentPasted0">* Integration of diverse formal methods techniques</div>
<div class="ContentPasted0">* Combination of formal methods with simulation and analysis techniques</div>
<div><br class="ContentPasted0">
</div>
<div class="ContentPasted0">Formal Methods in Practice</div>
<div class="ContentPasted0">* Experience reports of application of formal methods in industry</div>
<div class="ContentPasted0">* Use of formal methods in education</div>
<div class="ContentPasted0">* Applications of formal methods in:</div>
<div class="ContentPasted0"> - concurrent and distributed systems</div>
<div class="ContentPasted0"> - fault-detection, diagnostics, and prognostics systems</div>
<div class="ContentPasted0"> - human-machine interaction analysis</div>
<div><br class="ContentPasted0">
</div>
<div class="ContentPasted0">Safety Assurance of Autonomous Systems</div>
<div class="ContentPasted0">* Verification of machine learning (ML) enabled systems</div>
<div class="ContentPasted0">* Runtime monitoring or model checking to ensure safe operation</div>
<div class="ContentPasted0">* Formal specifications and modeling of ML enabled systems</div>
<div class="ContentPasted0">* Case-studies/experience reports exploring the application of formal methods
</div>
<div class="ContentPasted0"> in autonomous safety-critical, cyber-physical and hybrid systems</div>
<div class="ContentPasted0">* Using formal evidence for certification of ML enabled systems</div>
<div><br class="ContentPasted0">
</div>
<div class="ContentPasted0">Formal Methods for Digital Transformation</div>
<div class="ContentPasted0">* Applications related to Digital Twin & Digital Thread</div>
<div class="ContentPasted0">* Verification for integrated design and manufacturing</div>
<div class="ContentPasted0">* AI digital assistants for system design</div>
<div class="ContentPasted0">* Runtime monitoring for Smart Campus & Smart Cities</div>
<div><br class="ContentPasted0">
</div>
<div class="ContentPasted0">Accessibility of Formal Methods for New Industries</div>
<div class="ContentPasted0">* "New Space" markets </div>
<div class="ContentPasted0">* Advanced Air Mobility and Startup Aviation</div>
<div class="ContentPasted0">* Formal Methods as a Service</div>
<div><br class="ContentPasted0">
</div>
<div class="ContentPasted0">--------------------------------------------------</div>
<div class="ContentPasted0">Submissions:</div>
<div class="ContentPasted0">--------------------------------------------------</div>
<div><br class="ContentPasted0">
</div>
<div class="ContentPasted0">There are two categories of submissions:</div>
<div class="ContentPasted0">* Regular Papers (15 pages including references), describing fully developed
</div>
<div class="ContentPasted0"> work and complete results</div>
<div class="ContentPasted0">* Short Papers (6 pages including references), in one of the categories below:
</div>
<div class="ContentPasted0"> - Tool papers describing novel and publicly available tools</div>
<div class="ContentPasted0"> - Case studies detailing applications of formal methods</div>
<div class="ContentPasted0"> - New emerging ideas in the topics of interest</div>
<div><br class="ContentPasted0">
</div>
<div class="ContentPasted0">All papers should be in English and describe original work that has not been
</div>
<div class="ContentPasted0">published or submitted elsewhere. NFM24 will be a hybrid conference. Authors of</div>
<div class="ContentPasted0">accepted papers are encouraged to present their work in person at the
</div>
<div class="ContentPasted0">conference. </div>
<div><br class="ContentPasted0">
</div>
<div class="ContentPasted0">There will be a tool demonstration session at the conference, where tool
</div>
<div class="ContentPasted0">developers get to showcase their tools interactively with the attendees. All
</div>
<div class="ContentPasted0">tool papers, under the short papers category, are required to participate in
</div>
<div class="ContentPasted0">the tool demonstration session. Authors of regular papers are also welcome to
</div>
<div class="ContentPasted0">participate in the tool demonstration session to showcase their application.
</div>
<div><br class="ContentPasted0">
</div>
<div class="ContentPasted0">All submitters who are interested in participating in the tool demonstration
</div>
<div class="ContentPasted0">session must include an additional appendix (maximum 4 pages and will not
</div>
<div class="ContentPasted0">appear in the proceedings) containing the description of the proposed demo and
</div>
<div class="ContentPasted0">the URL to a screencast demonstrating the tool. Authors of all accepted papers
</div>
<div class="ContentPasted0">additionally have an opportunity to present a poster.
</div>
<div><br class="ContentPasted0">
</div>
<div class="ContentPasted0">NFM prohibits the use of generative AI to create the textual narrative of the
</div>
<div class="ContentPasted0">paper. However, the use of generative AI to create examples (such as text,
</div>
<div class="ContentPasted0">tables, graphics, and code) that support the paper is permitted, but this must
</div>
<div class="ContentPasted0">be disclosed in the paper. Basic word processing systems that recommend and
</div>
<div class="ContentPasted0">insert replacement text, perform spelling or grammar checks and corrections, or</div>
<div class="ContentPasted0">systems that do language translations need not be disclosed in the paper.</div>
<div><br class="ContentPasted0">
</div>
<div class="ContentPasted0">All submissions will be fully reviewed by members of the Program Committee.
</div>
<div class="ContentPasted0">Accepted regular and short papers will be published in the Formal Methods
</div>
<div class="ContentPasted0">subline of Springer’s Lecture Notes in Computer Science (LNCS) and must use
</div>
<div class="ContentPasted0">LNCS style formatting described on </div>
<div class="ContentPasted0">https://www.springer.com/gp/computer-science/lncs/conference-proceedings-guidelines.
</div>
<div class="ContentPasted0">Papers must be submitted in PDF format at the EasyChair submission site,
</div>
<div class="ContentPasted0">https://easychair.org/conferences/?conf=nfm2024.</div>
<div><br class="ContentPasted0">
</div>
<div class="ContentPasted0">--------------------------------------------------</div>
<div class="ContentPasted0">Location and Cost:</div>
<div class="ContentPasted0">--------------------------------------------------</div>
<div><br class="ContentPasted0">
</div>
<div class="ContentPasted0">The symposium will take place at the NASA Ames Conference Center,</div>
<div class="ContentPasted0">Moffett Field, California, USA.</div>
<div><br class="ContentPasted0">
</div>
<div class="ContentPasted0">There will be no registration fee charged to participants. All</div>
<div class="ContentPasted0">interested individuals, including non-US citizens, are welcome to</div>
<div class="ContentPasted0">attend, listen to the talks, and participate in discussions. However,</div>
<div class="ContentPasted0">all attendees must register.</div>
<div><br class="ContentPasted0">
</div>
<div><br class="ContentPasted0">
</div>
<div class="ContentPasted0">Nathan Benz</div>
<div class="ContentPasted0">Divya Gopinath</div>
<div class="ContentPasted0">Nija Shi</div>
<div><br class="ContentPasted0">
</div>
<div class="ContentPasted0">NFM '24 Chairs</div>
<div class="ContentPasted0">nfm24-chairs@lists.nasa.gov</div>
<br>
</div>
<div id="appendonsend"></div>
<hr style="display:inline-block;width:98%" tabindex="-1">
<div id="divRplyFwdMsg" dir="ltr"><font face="Calibri, sans-serif" style="font-size:11pt" color="#000000"><b>From:</b> Gopinath, Divya (ARC-TI)[KBR Wyle Services, LLC]<br>
<b>Sent:</b> Monday, September 25, 2023 8:53 AM<br>
<b>To:</b> agents@cs.umbc.edu <agents@cs.umbc.edu><br>
<b>Subject:</b> NFM 2024 Call For Papers</font>
<div> </div>
</div>
<style type="text/css" style="display:none">
<!--
p
{margin-top:0;
margin-bottom:0}
-->
</style>
<div dir="ltr">
<div><span style="font-family:Calibri,Arial,Helvetica,sans-serif; display:inline!important; color:rgb(0,0,0); background-color:rgb(255,255,255)">The 16th NASA Formal Methods Symposium</span></div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
NFM 2024</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
<br>
</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
June 4-6, 2024</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
Moffett Field, California</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
<br>
</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
--------------------------------------------------</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
Important Dates:</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
--------------------------------------------------</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
<br>
</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
Abstract submission: December 1, 2023</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
Full paper submission: December 8, 2023</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
Notification: February 16, 2024</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
Camera-ready version: March 15, 2024</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
<br>
</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
--------------------------------------------------</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
Theme of the Symposium:</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
--------------------------------------------------</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
<br>
</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
The widespread use and increasing complexity of mission-critical and</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
safety-critical systems at NASA and in the aerospace industry requires advanced</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
technologies to address their specification, design, verification, validation,</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
and certification processes. For example, there is an increasing need for</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
autonomous systems in deep space missions including NASA’s Moon to Mars</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
exploration plans. The NASA Formal Methods Symposium is a forum to foster</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
collaboration between theoreticians and practitioners from NASA, other</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
government agencies, academia, and industry, with the goal of identifying</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
challenges and providing solutions towards achieving assurance for such</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
critical systems. The focus of this symposium is on formal techniques for</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
software and system assurance for applications in space, aviation, robotics,</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
and other NASA-relevant safety-critical systems. This year’s symposium extends</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
the focus to safety assurance of machine learning enabled autonomous systems,</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
formal methods for digital transformation, and accessibility for new</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
industries.</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
<br>
</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
--------------------------------------------------</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
Topics of Interest:</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
--------------------------------------------------</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
<br>
</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
Advances in Formal Methods</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
* Formal verification, model checking, and static analysis</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
* Interactive and automated theorem proving</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
* Program and specification synthesis, code transformation and generation</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
* Run-time verification and test case generation</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
* Techniques and algorithms for scaling formal methods</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
* Design for verification and correct-by-design techniques</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
* Requirements generation, specification, and validation</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
<br>
</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
Safety Assurance of Autonomous Systems</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
* Verification of machine learning (ML) enabled systems</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
* Run-time monitoring or model checking to ensure safe operation</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
* Formal specifications and modeling of ML enabled systems</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
* Case-studies/experience reports exploring the application of formal methods</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
in autonomous safety-critical, cyber-physical and hybrid systems</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
* Using formal evidence for certification of ML enabled systems</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
<br>
</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
Formal Methods in Practice</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
* Experience reports of application of formal methods in industry</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
* Use of formal methods in education</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
* Applications of formal methods in:</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
- concurrent and distributed systems</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
- fault-detection, diagnostics, and prognostics systems</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
- human-machine interaction analysis</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
<br>
</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
Safety Assurance of Autonomous Systems</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
* Verification of machine learning (ML) enabled systems</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
* Runtime monitoring or model checking to ensure safe operation</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
* Formal specifications and modeling of ML enabled systems</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
* Case-studies/experience reports exploring the application of formal methods</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
in autonomous safety-critical, cyber-physical and hybrid systems</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
* Using formal evidence for certification of ML enabled systems</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
<br>
</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
Formal Methods for Digital Transformation</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
* Applications related to Digital Twin & Digital Thread</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
* Verification for integrated design and manufacturing</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
* AI digital assistants for system design</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
* Runtime monitoring for Smart Campus & Smart Cities</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
<br>
</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
Accessibility of Formal Methods for New Industries</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
* "New Space" markets</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
* Advanced Air Mobility and Startup Aviation</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
* Formal Methods as a Service</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
<br>
</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
--------------------------------------------------</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
Submissions:</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
--------------------------------------------------</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
<br>
</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
There are two categories of submissions:</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
* Regular Papers (15 pages) including references, describing fully developed</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
work and complete results</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
* Short Papers (6 pages) including references, in one of the categories below:</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
- Tool papers describing novel and publicly available tools</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
- Case studies detailing applications of formal methods</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
- New emerging ideas in the topics of interest</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
<br>
</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
All papers should be in English and describe original work that has not been</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
published or submitted elsewhere. NFM24 will be a hybrid conference. Authors of</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
accepted papers are encouraged to present their work in person at the</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
conference.</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
<br>
</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
There will be a tool demonstration session at the conference, where tool</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
developers get to showcase their tools interactively with the attendees. All</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
tool papers, under the short papers category, are required to participate in</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
the tool demonstration session. uthors of regular papers are also welcome to</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
participate in the tool demonstration session to showcase their application.</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
<br>
</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
All submitters who are interested in participating in the tool demonstration</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
session must include an additional appendix (maximum 4 pages and will not</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
appear in the proceedings) containing the description of the proposed demo and</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
the URL to a screencast demonstrating the tool. Authors of all accepted papers</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
additionally have an opportunity to present a poster.</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
<br>
</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
All submissions will be fully reviewed by members of the Program Committee.</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
Accepted regular and short papers will be published in the Formal Methods</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
subline of Springer’s Lecture Notes in Computer Science (LNCS) and must use</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
LNCS style formatting described on</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
<a href="https://www.springer.com/gp/computer-science/lncs/conference-proceedings-guidelines" class="x_ms-outlook-linkify x_OWAAutoLink" target="_blank" id="OWA4cf1a695-cac6-059e-7d88-4c7d97d33aa0" style="margin:0px">https://www.springer.com/gp/computer-science/lncs/conference-proceedings-guidelines</a>.</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
Papers must be submitted in PDF format at the EasyChair submission site,</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
<a href="https://easychair.org/conferences/?conf=nfm2024" class="x_ms-outlook-linkify x_OWAAutoLink" target="_blank" id="OWAf5b3a01b-4d77-676d-344f-f9d1c01ec214" style="margin:0px">https://easychair.org/conferences/?conf=nfm2024</a>.</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
<br>
</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
--------------------------------------------------</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
Location and Cost:</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
--------------------------------------------------</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
<br>
</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
The symposium will take place at the NASA Ames Conference Center,</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
Moffett Field, California, USA.</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
<br>
</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
There will be no registration fee charged to participants. All</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
interested individuals, including non-US citizens, are welcome to</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
attend, listen to the talks, and participate in discussions. However,</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
all attendees must register.</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
<br>
</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
<br>
</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
Nathan Benz</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
Divya Gopinath</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
Nija Shi</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
<br>
</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
NFM '24 Chairs</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; margin:0px; color:rgb(0,0,0); background-color:rgb(255,255,255)">
nfm24-chairs@lists.nasa.gov</div>
<div class="x_elementToProof" style="font-family:Calibri,Arial,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0)">
<br>
</div>
</div>
</body>
</html>