<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class="">
<div class=""><br class="">
</div>
<div class="">
<div class="" style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt; text-align: center;">
<span class="" style="font-size: 12.6667px; font-family: Arial; color: rgb(34, 34, 34); background-color: rgb(255, 255, 255); vertical-align: baseline;">NFM 2017 - Call For Papers</span></div>
<br class="">
<div class="" style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt; text-align: center;">
<span class="" style="font-size: 12.6667px; font-family: Arial; color: rgb(34, 34, 34); background-color: rgb(255, 255, 255); vertical-align: baseline;">The 9th NASA Formal Methods Symposium</span></div>
<div class="" style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt; text-align: center;">
<span class="" style="font-size: 12.6667px; font-family: Arial; color: rgb(34, 34, 34); background-color: rgb(255, 255, 255); vertical-align: baseline;">-------------------------------------</span></div>
<div class="" style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt; text-align: center;">
<span class="" style="font-size: 12.6667px; font-family: Arial; color: rgb(34, 34, 34); background-color: rgb(255, 255, 255); vertical-align: baseline;"><a href="http://ti.arc.nasa.gov/events/nfm-2017/" class="">http://ti.arc.nasa.gov/events/nfm-2017/</a></span></div>
<div class="" style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt; text-align: center;">
<span class="" style="font-size: 12.6667px; font-family: Arial; color: rgb(34, 34, 34); background-color: rgb(255, 255, 255); vertical-align: baseline;">May 16 - 18, 2017</span></div>
<div class="" style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt; text-align: center;">
<span class="" style="font-size: 12.6667px; font-family: Arial; color: rgb(34, 34, 34); background-color: rgb(255, 255, 255); vertical-align: baseline;">NASA Ames Research Center</span></div>
<div class="" style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt; text-align: center;">
<span class="" style="font-size: 12.6667px; font-family: Arial; color: rgb(34, 34, 34); background-color: rgb(255, 255, 255); vertical-align: baseline;">Moffett Field, CA, USA</span></div>
<br class="">
<div class="" style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;"><span class="" style="font-size: 12.6667px; font-family: Arial; color: rgb(34, 34, 34); background-color: rgb(255, 255, 255); vertical-align: baseline;">Theme of the Symposium</span></div>
<div class="" style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;"><span class="" style="font-size: 12.6667px; font-family: Arial; color: rgb(34, 34, 34); background-color: rgb(255, 255, 255); vertical-align: baseline;">----------------------</span></div>
<br class="">
<div class="" style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;"><span class="" style="font-size: 12.6667px; font-family: Arial; color: rgb(34, 34, 34); background-color: rgb(255, 255, 255); vertical-align: baseline;">The widespread use and increasing
complexity of mission-critical and safety-critical systems at NASA and in the aerospace industry require advanced techniques that address these systems’ specification, design, verification, validation, and certification requirements. The NASA Formal Methods
Symposium (NFM) is a forum to foster collaboration between theoreticians and practitioners from NASA, academia, and industry. NFM’s goals are to identify challenges and to provide solutions for achieving assurance for such critical systems.</span></div>
<br class="">
<div class="" style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;"><span class="" style="font-size: 12.6667px; font-family: Arial; color: rgb(34, 34, 34); background-color: rgb(255, 255, 255); vertical-align: baseline;">New developments and emerging
applications like autonomous 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.</span></div>
<br class="">
<div class="" style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;"><span class="" style="font-size: 12.6667px; font-family: Arial; color: rgb(34, 34, 34); background-color: rgb(255, 255, 255); vertical-align: baseline;">The focus of the symposium
will be on formal techniques and other approaches for software assurance, including 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.</span></div>
<div class="" style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;"><br class="">
</div>
<br class="">
<div class="" style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;"><span class="" style="font-size: 12.6667px; font-family: Arial; color: rgb(34, 34, 34); background-color: rgb(255, 255, 255); vertical-align: baseline;">Topics of interest include
but are not limited to:</span></div>
<div class="" style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;"><span class="" style="font-size: 12.6667px; font-family: Arial; color: rgb(34, 34, 34); background-color: rgb(255, 255, 255); vertical-align: baseline;">-------------------------------------------------</span></div>
<div class="" style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;"><span class="" style="font-size: 12.6667px; font-family: Arial; color: rgb(34, 34, 34); background-color: rgb(255, 255, 255); vertical-align: baseline;">* Model checking</span></div>
<div class="" style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;"><span class="" style="font-size: 12.6667px; font-family: Arial; color: rgb(34, 34, 34); background-color: rgb(255, 255, 255); vertical-align: baseline;">* Theorem proving</span></div>
<div class="" style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;"><span class="" style="font-size: 12.6667px; font-family: Arial; color: rgb(34, 34, 34); background-color: rgb(255, 255, 255); vertical-align: baseline;">* SAT and SMT solving</span></div>
<div class="" style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;"><span class="" style="font-size: 12.6667px; font-family: Arial; color: rgb(34, 34, 34); background-color: rgb(255, 255, 255); vertical-align: baseline;">* Symbolic execution</span></div>
<div class="" style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;"><span class="" style="font-size: 12.6667px; font-family: Arial; color: rgb(34, 34, 34); background-color: rgb(255, 255, 255); vertical-align: baseline;">* Static analysis</span></div>
<div class="" style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;"><span class="" style="font-size: 12.6667px; font-family: Arial; color: rgb(34, 34, 34); background-color: rgb(255, 255, 255); vertical-align: baseline;">* Model-based development</span></div>
<div class="" style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;"><span class="" style="font-size: 12.6667px; font-family: Arial; color: rgb(34, 34, 34); background-color: rgb(255, 255, 255); vertical-align: baseline;">* Runtime verification</span></div>
<div class="" style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;"><span class="" style="font-size: 12.6667px; font-family: Arial; color: rgb(34, 34, 34); background-color: rgb(255, 255, 255); vertical-align: baseline;">* Software and system testing</span></div>
<div class="" style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;"><span class="" style="font-size: 12.6667px; font-family: Arial; color: rgb(34, 34, 34); background-color: rgb(255, 255, 255); vertical-align: baseline;">* Safety assurance</span></div>
<div class="" style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;"><span class="" style="font-size: 12.6667px; font-family: Arial; color: rgb(34, 34, 34); background-color: rgb(255, 255, 255); vertical-align: baseline;">* Fault tolerance</span></div>
<div class="" style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;"><span class="" style="font-size: 12.6667px; font-family: Arial; color: rgb(34, 34, 34); background-color: rgb(255, 255, 255); vertical-align: baseline;">* Compositional verification</span></div>
<div class="" style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;"><span class="" style="font-size: 12.6667px; font-family: Arial; color: rgb(34, 34, 34); background-color: rgb(255, 255, 255); vertical-align: baseline;">* Security and intrusion detection</span></div>
<div class="" style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;"><span class="" style="font-size: 12.6667px; font-family: Arial; color: rgb(34, 34, 34); background-color: rgb(255, 255, 255); vertical-align: baseline;">* Design for verification
and correct-by-design techniques</span></div>
<div class="" style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;"><span class="" style="font-size: 12.6667px; font-family: Arial; color: rgb(34, 34, 34); background-color: rgb(255, 255, 255); vertical-align: baseline;">* Techniques for scaling formal
methods</span></div>
<div class="" style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;"><span class="" style="font-size: 12.6667px; font-family: Arial; color: rgb(34, 34, 34); background-color: rgb(255, 255, 255); vertical-align: baseline;">* Formal methods for multi-core,
GPU-based implementations</span><span class="" style="font-family: Arial; color: rgb(34, 34, 34); background-color: rgb(255, 255, 255); vertical-align: baseline;"></span></div>
<div class="" style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;"><span class="" style="font-size: 12.6667px; font-family: Arial; color: rgb(34, 34, 34); background-color: rgb(255, 255, 255); vertical-align: baseline;">* Applications of formal methods
in the development of:</span></div>
<div class="" style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;"><span class="" style="font-size: 12.6667px; font-family: Arial; color: rgb(34, 34, 34); background-color: rgb(255, 255, 255); vertical-align: baseline;"> * autonomous systems</span></div>
<div class="" style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;"><span class="" style="font-size: 12.6667px; font-family: Arial; color: rgb(34, 34, 34); background-color: rgb(255, 255, 255); vertical-align: baseline;"> * safety-critical artificial
intelligence systems</span></div>
<div class="" style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;"><span class="" style="font-size: 12.6667px; font-family: Arial; color: rgb(34, 34, 34); background-color: rgb(255, 255, 255); vertical-align: baseline;"> * cyber-physical, embedded,
and hybrid systems</span></div>
<div class="" style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;"><span class="" style="font-size: 12.6667px; font-family: Arial; color: rgb(34, 34, 34); background-color: rgb(255, 255, 255); vertical-align: baseline;"> * fault-detection, diagnostics,
and prognostics systems</span></div>
<br class="">
<div class="" style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;"><span class="" style="font-size: 12.6667px; font-family: Arial; color: rgb(34, 34, 34); background-color: rgb(255, 255, 255); vertical-align: baseline;">* Use of formal methods in:</span></div>
<div class="" style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;"><span class="" style="font-size: 12.6667px; font-family: Arial; color: rgb(34, 34, 34); background-color: rgb(255, 255, 255); vertical-align: baseline;"> * assurance cases</span></div>
<div class="" style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;"><span class="" style="font-size: 12.6667px; font-family: Arial; color: rgb(34, 34, 34); background-color: rgb(255, 255, 255); vertical-align: baseline;"> * human-machine interaction
analysis</span></div>
<div class="" style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;"><span class="" style="font-size: 12.6667px; font-family: Arial; color: rgb(34, 34, 34); background-color: rgb(255, 255, 255); vertical-align: baseline;"> * requirements generation,
specification, and validation</span></div>
<div class="" style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;"><span class="" style="font-size: 12.6667px; font-family: Arial; color: rgb(34, 34, 34); background-color: rgb(255, 255, 255); vertical-align: baseline;"> * automated testing and
verification</span></div>
<br class="">
<div class="" style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;"><span class="" style="font-size: 12.6667px; font-family: Arial; color: rgb(34, 34, 34); background-color: rgb(255, 255, 255); vertical-align: baseline;">Important Dates</span></div>
<div class="" style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;"><span class="" style="font-size: 12.6667px; font-family: Arial; color: rgb(34, 34, 34); background-color: rgb(255, 255, 255); vertical-align: baseline;">---------------</span></div>
<div class="" style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;"><span class="" style="font-size: 12.6667px; font-family: Arial; color: rgb(34, 34, 34); background-color: rgb(255, 255, 255); vertical-align: baseline;">Abstract Submission: November
28, 2016</span></div>
<div class="" style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;"><span class="" style="font-size: 12.6667px; font-family: Arial; color: rgb(34, 34, 34); background-color: rgb(255, 255, 255); vertical-align: baseline;">Paper Submission: December
5, 2016</span></div>
<div class="" style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;"><span class="" style="font-size: 12.6667px; font-family: Arial; color: rgb(34, 34, 34); background-color: rgb(255, 255, 255); vertical-align: baseline;">Paper notification: February
3, 2017</span></div>
<div class="" style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;"><span class="" style="font-size: 12.6667px; font-family: Arial; color: rgb(34, 34, 34); background-color: rgb(255, 255, 255); vertical-align: baseline;">Camera Ready Deadline: March
1, 2017</span></div>
<div class="" style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;"><span class="" style="font-size: 12.6667px; font-family: Arial; color: rgb(34, 34, 34); background-color: rgb(255, 255, 255); vertical-align: baseline;">Symposium: May 16-18, 2017</span></div>
<br class="">
<div class="" style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;"><span class="" style="font-size: 12.6667px; font-family: Arial; color: rgb(34, 34, 34); background-color: rgb(255, 255, 255); vertical-align: baseline;">Location</span></div>
<div class="" style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;"><span class="" style="font-size: 12.6667px; font-family: Arial; color: rgb(34, 34, 34); background-color: rgb(255, 255, 255); vertical-align: baseline;">--------</span></div>
<div class="" style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;"><span class="" style="font-size: 12.6667px; font-family: Arial; color: rgb(34, 34, 34); background-color: rgb(255, 255, 255); vertical-align: baseline;">The symposium will take place
at NASA Ames Research Center, Moffett Field, CA, USA.</span></div>
<div class="" style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;"><span class="" style="font-size: 12.6667px; font-family: Arial; color: rgb(34, 34, 34); background-color: rgb(255, 255, 255); vertical-align: baseline;">Registration is required but
is free of charge.</span></div>
<br class="">
<div class="" style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;"><span class="" style="font-size: 12.6667px; font-family: Arial; color: rgb(34, 34, 34); background-color: rgb(255, 255, 255); vertical-align: baseline;">Submission Details</span></div>
<div class="" style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;"><span class="" style="font-size: 12.6667px; font-family: Arial; color: rgb(34, 34, 34); background-color: rgb(255, 255, 255); vertical-align: baseline;">------------------</span></div>
<div class="" style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;"><span class="" style="font-size: 12.6667px; font-family: Arial; color: rgb(34, 34, 34); background-color: rgb(255, 255, 255); vertical-align: baseline;">There are two categories of
submissions:</span></div>
<br class="">
<div class="" style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;"><span class="" style="font-size: 12.6667px; font-family: Arial; color: rgb(34, 34, 34); background-color: rgb(255, 255, 255); vertical-align: baseline;">1. Regular papers describing
fully developed work and complete results (maximum 15 pages)</span></div>
<br class="">
<div class="" style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;"><span class="" style="font-size: 12.6667px; font-family: Arial; color: rgb(34, 34, 34); background-color: rgb(255, 255, 255); vertical-align: baseline;">2. Short papers on tools,
experience reports, or work in progress with preliminary results (maximum 6 pages)</span></div>
<br class="">
<div class="" style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;"><span class="" style="font-size: 12.6667px; font-family: Arial; color: rgb(34, 34, 34); background-color: rgb(255, 255, 255); vertical-align: baseline;">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.</span></div>
<br class="">
<div class="" style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;"><span class="" style="font-size: 12.6667px; font-family: Arial; color: rgb(34, 34, 34); background-color: rgb(255, 255, 255); vertical-align: baseline;">Papers will appear in a volume
of Springer's Lecture Notes in Computer Science (LNCS), and must </span></div>
</div>
</body>
</html>