NFM 2024NASA Formal Methods 2024

16th NASA Formal Methods Symposium June 4-6

The NASA Formal Methods Symposium (NFM) is an annual forum to foster collaboration between theoreticians and practitioners from NASA, other government agencies, academia, and industry.

Updates

NFM 2024 has now concluded. Thanks to all participants for making this a successful conference! (6/7/24)

Social events and lunch options announced (5/31/24)

Registration for all foreign nationals who want to attend the symposium physically is now closed due to the time it takes to process each visitor request. Registration is still open for US persons to attend physically and anyone who wants to attend virtually. Please note that a visa to the US is no longer required for foreign nationals to attend the symposium virtually. Please follow this link to register. (5/15/2024)

NFM Schedule is now available (4/17/2024)

Keynote talks announced (4/5/24)

Please check out more information about the venue (3/8/24)

Registration now open (2/26/24)

Notification Date Extended (2/17/24)

Notifications will be sent out on February 18

FAQ page available for your questions (12/5/23)

Submission Deadlines Extended (12/1/23)

• Abstract Submission: December 8
• Full Paper Submission: December 15

Updated CFP with NFM Policy on use of Generative AI (10/30/23)

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.

Download Call for Papers PDF

Highlights

Keynote

Autonomy Challenges for Future NASA Science and Exploration Missions

Butler Hine

Keynote

Safety under uncertainty: Automotive standards for AI safety and research perspectives

Simon Burton

Keynote

Formal Verification and Run-time Monitoring for Learning-Enabled Autonomous Systems

Corina S. Pasareanu

Supporters

Events

Call for Papers

Download Call for Papers PDF

Theme of the Symposium

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 processes. For example, there is an increasing need for autonomous systems in deep space missions including NASA’s Moon to Mars exploration plans. 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 safety-critical systems. This year’s symposium extends the focus to safety assurance of machine learning enabled autonomous systems, formal methods for digital transformation, and accessibility for new industries.

Topics of Interest

Advances in Formal Methods

• Formal verification, model checking, 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

Integration of Formal Methods

• Use of machine learning techniques in formal methods
• Integration of formal methods and software engineering
• Integration of diverse formal methods techniques
• Combination of formal methods with simulation and analysis techniques

Formal Methods in Practice

• Experience reports of application of formal methods in industry
• Use of formal methods in education
• Applications of formal methods in:
  • concurrent and distributed systems
  • fault-detection, diagnostics, and prognostics systems
  • human-machine interaction analysis

Safety Assurance of Autonomous Systems

• Verification of machine learning (ML) enabled systems
• Runtime monitoring or model checking to ensure safe operation
• Formal specifications and modeling of ML enabled systems
• Case-studies/experience reports exploring the application of formal methods in autonomous safety-critical, cyber-physical and hybrid systems
• Using formal evidence for certification of ML enabled systems

Formal Methods for Digital Transformation

• Applications related to Digital Twin & Digital Thread
• Verification for integrated design and manufacturing
• AI digital assistants for system design
• Runtime monitoring for Smart Campus & Smart Cities

Accessibility of Formal Methods for New Industries

• “New Space” markets
• Advanced Air Mobility and Startup Aviation
• Formal Methods as a Service

Submissions

There are two categories of submissions:

• Regular Papers (15 pages including references), describing fully developed work and complete results
• Short Papers (6 pages including references), in one of the categories below:
  • Tool papers describing novel and publicly available tools
  • Case studies detailing applications of formal methods
  • New emerging ideas in the topics of interest

All papers should be in English and describe original work that has not been published or submitted elsewhere. NFM24 will be a hybrid conference. Authors of accepted papers are encouraged to present their work in person at the conference.

There will be a tool demonstration session at the conference, where tool developers get to showcase their tools interactively with the attendees. All tool papers, under the short papers category, are required to participate in the tool demonstration session. Authors of regular papers are also welcome to participate in the tool demonstration session to showcase their application.

All submitters who are interested in participating in the tool demonstration session must include an additional appendix (maximum 4 pages and will not appear in the proceedings) containing the description of the proposed demo and the URL to a screencast demonstrating the tool. Authors of all accepted papers additionally have an opportunity to present a poster.

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.

All submissions will be fully reviewed by members of the Program Committee. Accepted regular and short papers will be published in the Formal Methods subline of Springer’s Lecture Notes in Computer Science (LNCS) and must use LNCS style formatting described on https://www.springer.com/gp/computer-science/lncs/conference-proceedings-guidelines. Papers must be submitted in PDF format at the EasyChair submission site, https://easychair.org/conferences/?conf=nfm2024.

Location and Cost

The symposium will take place at the NASA Ames Conference Center, Moffett Field, California, USA.

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.

About submitting a tool paper under the short paper category

What are the submission requirements?

All tool papers, under the short paper category, must include an additional appendix (maximum 4 pages and will not appear in the proceedings) containing the description of the proposed demo and the URL to a screencast demonstrating the tool.

What is the format of the screencast?

There are no restrictions on the format and length of the screencast. The purpose of the screencast is to help our reviewers understand the tool.

How will NFM24 use the screencast?

Screencast(s) included in a submission will only be used by our program committee during the review process.

What are the presentation requirements?

All tool papers, under the short papers category, are required to participate in the tool demonstration session. Depending on our program schedule, we might invite each presenter to give a 5-minute lightning presentation in the main session.

What is the format of the tool demonstration session?

The tool demonstration session will be held in a showroom, where each presenter will have a kiosk and, depending on availability, an external monitor, for their demonstration along with other presenters at the same time. Presenters will be demonstrating their tools while interacting with the attendees during the session.

Still can’t find what you’re looking for? Contact us!

The online proceedings for NFM 2024 are published in the Formal Methods subline of Springer’s Lecture Notes in Computer Science (LNCS)