April 27-29, 2015, Pasadena, California, USA
Submission deadline: November 10, 2014
The widespread use and increasing complexity of mission- and safety-critical systems require advanced techniques that address their specification, verification, validation, and certification.
The NASA Formal Methods Symposium is a forum for theoreticians and practitioners from academia, industry, and government, with the goals of identifying challenges and providing solutions to achieving assurance in mission- and safety-critical systems. Within NASA such systems include for example autonomous robots, separation assurance algorithms for aircraft, Next Generation Air Transportation (NextGen), and autonomous rendezvous and docking for spacecraft. Moreover, emerging paradigms such as property-based design, 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 mission- and safety-critical systems in all design life-cycle stages. We encourage submissions on cross-cutting approaches marrying formal verification techniques with advances in critical system development, such as requirements generation, analysis of aerospace operational concepts, and formal methods integrated in early design stages and carrying throughout system development.
Topics of interest
Symposium topics of interest include but are not limited to the following:
- Model checking
- Theorem proving
- SAT and SMT solving
- Symbolic execution
- Static analysis
- Runtime verification
- Program refinement
- Compositional verification
- Security and intrusion detection
- Modeling and specification formalisms
- Model-based development
- Model-based testing
- Requirement engineering
- Formal approaches to fault tolerance
- Applications of formal methods to aerospace systems
- Applications of formal methods to cyber-physical systems
- Applications of formal methods to human-machine interaction analysis
There will not be a registration fee charged to participants. All interested individuals, including non-US citizens, are welcome to submit, to attend, to listen to the talks, and to participate in discussions; however, all attendees must register. The registration website will be activated closer to the event.
NFM 2015 is organized by Laboratory for Reliable Software (LaRS) at NASA’s Jet Propulsion Laboratory (JPL). JPL is a federally funded research and development center and NASA field center, managed by the nearby California Institute of Technology (Caltech) for the National Aeronautics and Space Administration. The laboratory’s primary function is the construction and operation of planetary robots and spacecraft, for example the Mars rovers.
NFM 2015 is the seventh edition of the NASA Formal Methods Symposium, steered by the NASA Formal Methods Group. The symposium grew out of a workshop series started by the NASA Langley Formal Methods Group, and is now held annually, hosted each year by one of the NASA centers.
Proceedings to be published in: