<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: Calibri, Arial, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);" class="elementToProof ContentPasted0">
The 16th NASA Formal Methods Symposium
<div class="ContentPasted0">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">--------------------------------------------------</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">Safety Assurance of Autonomous Systems </div>
<div class="ContentPasted0">* Verification of machine learning (ML) enabled systems
</div>
<div class="ContentPasted0">* Run-time 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 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. uthors 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">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>
</body>
</html>