McNamara Alumni Center
University of Minnesota
200 Oak Street S.E., Minneapolis, MN 55455
Theme of the Symposium
The widespread use and increasing complexity of mission-critical and
safety-critical systems at NASA and the aerospace industry requires advanced
techniques that address their specification, design, verification, validation,
and certification requirements. The NASA Formal Methods Symposium is a forum
to foster collaboration between theoreticians and practitioners from NASA,
academia, and the industry, with the goal of identifying challenges and
providing solutions towards achieving assurance for such critical systems.
New developments and emerging applications like autonomous on-board software
for Unmanned Aerial Systems (UAS), UAS Traffic Management (UTM), advanced
separation assurance algorithms for aircraft, and the need for system-wide
fault detection, diagnosis, and prognostics provide new challenges for system
specification, development, and verification approaches. Similar challenges
need to be addressed during development and deployment of on-board software
for spacecraft ranging from small and inexpensive CubeSat systems to manned
spacecraft like Orion, as well as for ground systems.
The focus of the symposium will be on formal techniques and other approaches
for software assurance, their theory, current capabilities and limitations,
as well as their potential application to aerospace, robotics, and other
NASA-relevant safety-critical systems during all stages of the software
life-cycle.
Topics of interest include but are not limited to
Model checking
Theorem proving
SAT and SMT solving
Symbolic execution
Static analysis
Model-based development
Runtime verification
Software and system testing
Safety assurance
Fault tolerance
Compositional verification
Security and intrusion detection
Design for verification and correct-by-design techniques
Techniques for scaling formal methods
Applications of formal methods in the development of:
autonomous systems
safety-critical artificial intelligence systems
cyber-physical, embedded, and hybrid systems
fault-detection, diagnostics, and prognostics systems
Use of formal methods in:
assurance cases
human-machine interaction analysis
requirements generation, specification, and validation
automated testing and verification
Important Dates
Paper Submission: 2/19/2016
Paper Notifications: 4/8/2016
Camera-ready Papers: 4/27/2016
Symposium: 6/7 - 6/9/2016
Location
The symposium will take place at McNamara Alumni Center, University of
Minnesota.
Registration is required but is free of charge.
Submission Details
There are two categories of submissions:
Regular papers describing fully developed work and complete
results (maximum 15 pages)
Short papers on tools, experience reports, or work in progress
with preliminary results (maximum 6 pages)
All papers must be in English and describe original work that has not been
published or submitted elsewhere. All submissions will be fully reviewed by
at least three members of the Program Committee.
Papers will appear in a volume of Springer's Lecture Notes in Computer
Science
(LNCS), and must use LNCS style formatting. Papers must be submitted in PDF
format at the EasyChair submission site: