April 6 - 8, 2009 Moffett Field, California

The widespread use and increasing complexity of safety-critical systems require advanced techniques that address their verification and certification requirements.

NFM 2009 is a forum for theoreticians and practitioners from academia and industry, with the goals of identifying challenges and providing solutions to achieving assurance in safety-critical systems. Within NASA, for example, such systems include autonomous robots, separation assurance algorithms for aircraft, and autonomous rendezvous and docking for spacecraft. Moreover, emerging paradigms such as code generation and safety cases are bringing with them new challenges and opportunities.

The focus of the symposium will be on formal techniques, their theory, current capabilities, and limitations, as well as their application to aerospace, robotics, and other safety-critical systems. The symposium aims to introduce researchers, graduate students, and partners in industry to those topics that are of interest, to survey current research, and to identify unsolved problems and directions for future research.

The meeting will be comprised of invited talks by leading researchers and practitioners, a panel discussion on the current status of formal methods, and more specialized talks based on contributed papers.

The NASA Formal Methods Symposium is a new annual event intended to highlight the state of formal methods' art and practice. It follows the earlier Langley Formal Methods Workshop series and aims to foster collaboration between NASA researchers and engineers, as well as the wider aerospace, safety-critical and formal methods communities.

• Formal verification, including theorem proving, model checking, and static analysis
• Automated testing and simulation techniques
• Model-based development
• Techniques and algorithms for scaling formal methods, such as abstraction and symbolic methods, compositional techniques, as well as parallel and/or distributed techniques
• Code generation
• Safety cases
• Accident/safety analysis
• Formal approaches to fault tolerance
• Theoretical advances and empirical evaluations of formal methods techniques for safety-critical systems, including hybrid and embedded systems

• Ed Clarke, CMU
• Todd Farley, NASA Ames
• Leslie Lamport, Microsoft
• John O'Leary, Intel
• Bill Othon, NASA Johnson

• Regular papers describing fully developed work and complete results (10 pages / 30 minute talks)
• Short papers describing interesting work in progress and/or preliminary results (5 pages / 15 minute talks)

All papers should describe original work that has not been published elsewhere. Submissions will be fully reviewed and the symposium proceedings will appear as a NASA Conference Publication. Authors of selected papers will then be invited to submit extended versions to a special issue of "Innovations in Systems and Software Engineering: a NASA Journal" (Springer).

Papers should be submitted through the following link: http://www.easychair.org/conferences/?conf=nfm2009

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, to listen to the talks, and to participate in discussions. However, all attendees must register.

Last modified: Feb. 24, 2009.