Call for Papers 18th NASA Formal Methods Symposium (NFM’26) 5-7 May 2026 Los Angeles, CA
https://gcc02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fnfm2026.github.io%2F&data=05%7C02%7Cfm-announcements%40lists.nasa.gov%7C3ede4a2dd882408b6b1d08ddf6cdefc8%7C7005d45845be48ae8140d43da96dd17b%7C0%7C0%7C638938086547683908%7CUnknown%7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ%3D%3D%7C0%7C%7C%7C&sdata=zMt4aC0TQ5rIzWn6bDYfYaufTA4ZFxforeBO7BuBUSs%3D&reserved=0 --- Symposium Theme --- 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. --- Topics of Interest --- Core Formal Methods – Formal verification techniques like interactive and automated theorem proving, SAT/SMT solvers, model checking, and static analysis; logic-based specification formalisms; program and specification synthesis, code transformation and generation; runtime verification and test case generation; scenario-based testing; probabilistic/statistical methods; techniques and algorithms for scaling formal methods; design for verification and correct-by-design techniques; requirements generation, specification, and validation. Integration of 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; integration of learning-based techniques with formal methods; use of AI models (e.g., LLMs) in formal methods pipelines, and other neuro-symbolic methods. 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, distributed, and fault-tolerant systems, human-machine systems, autonomous systems, cyber-physical systems, fault-detection, diagnostics, and prognostics systems; formal reasoning about real-time systems, scheduling, and planning; and formal reasoning about artifacts generated by AI-based language models (such as LLMs, vision-language-action models, etc.). --- NASA OPEN SOURCE SOFTWARE --- Courageous authors, who want to delve in open source software being applied in real NASA missions, and find possible connections to, and applications of Formal Methods, are invited to visit the open source repositories for the following two frameworks for programming flight software: - F' (https://gcc02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fnasa.github.io%2Ffprime&data=05%7C02%7Cfm-announcements%40lists.nasa.gov%7C3ede4a2dd882408b6b1d08ddf6cdefc8%7C7005d45845be48ae8140d43da96dd17b%7C0%7C0%7C638938086547704326%7CUnknown%7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ%3D%3D%7C0%7C%7C%7C&sdata=4nYPZDiIHla2X94bJi0Xkt4xuOI3znemHC%2BA1VMINr0%3D&reserved=0) - cFS (https://cfs.gsfc.nasa.gov) --- Submission --- There are two categories of submissions: Regular papers – Up to 18 pages plus references. Regular papers describe fully developed work and complete results. 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. 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. Policy on the use of Gen AI: We understand the convenience afforded by the use of generative AI-based large language models to produce text in the submitted manuscript. However, we strongly encourage the authors to check the generated text for factual errors and inconsistencies. We encourage the authors to adopt appropriate standards for citing products obtained using generative AI (such as text, tables, graphics). Use of AI-based coding assistants is permitted, and we encourage authors to disclose the use of such tools as the community may find this scientifically interesting. All submissions will be fully reviewed by 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 https://gcc02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fwww.springer.com%2Fgp%2Fcomputer-science%2Flncs%2Fconference-proceedings-guidelines&data=05%7C02%7Cfm-announcements%40lists.nasa.gov%7C3ede4a2dd882408b6b1d08ddf6cdefc8%7C7005d45845be48ae8140d43da96dd17b%7C0%7C0%7C638938086547717848%7CUnknown%7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ%3D%3D%7C0%7C%7C%7C&sdata=U%2FzBXw3TZp1COFEI5aKMeOFWkqUlc4g8G9foQvVGk30%3D&reserved=0. Papers must be submitted in PDF format through the Openreview submission site here: https://gcc02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fopenreview.net%2Fgroup%3Fid%3DNFM%2F2026%2FSymposium&data=05%7C02%7Cfm-announcements%40lists.nasa.gov%7C3ede4a2dd882408b6b1d08ddf6cdefc8%7C7005d45845be48ae8140d43da96dd17b%7C0%7C0%7C638938086547731115%7CUnknown%7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ%3D%3D%7C0%7C%7C%7C&sdata=7xpuhN1UL2npugR%2F6V0HG2YG3okqo2LwJVuvW3KHjdM%3D&reserved=0. Detailed instructions on submitting papers through the Openreview submission system can be found on the NFM 2026 website. --- Important Dates --- Paper submission January 10, 2025 Author notification March 10, 2026 Camera ready deadline March 30, 2026 Symposium May 5-7, 2026 --- Location --- The symposium will be organized jointly by NASA Jet Propulsion Laboratory (JPL) and the Thomas Lord Department of Computer Science at the University of Southern California (USC). The symposium will be held on the campus of USC, which is around 3 miles south of downtown Los Angeles. USC is the largest private university in southern California, and is well-connected to the rest of the city by LA Metro. It is also close to a number of museums. --- Cost --- There will be no registration fee charged to participants as is common for NFM symposia. All interested individuals, including non-US citizens, are welcome to attend, listen to the talks, and participate in discussions. However, all attendees must register. --- end --- --- To opt-out from this mailing list, send an email to fm-announcements-requ...@lists.nasa.gov with the word 'unsubscribe' as subject or in the body. You can also make the request by contacting fm-announcements-ow...@lists.nasa.gov _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
