<html xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns="http://www.w3.org/TR/REC-html40"><head><meta http-equiv=Content-Type content="text/html; charset=utf-8"><meta name=Generator content="Microsoft Word 15 (filtered medium)"><style><!--
/* Font Definitions */
@font-face
{font-family:"Cambria Math";
panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
{font-family:Calibri;
panose-1:2 15 5 2 2 2 4 3 2 4;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0in;
font-size:11.0pt;
font-family:"Calibri",sans-serif;}
span.EmailStyle17
{mso-style-type:personal-compose;
font-family:"Calibri",sans-serif;
color:windowtext;}
.MsoChpDefault
{mso-style-type:export-only;
font-family:"Calibri",sans-serif;}
@page WordSection1
{size:8.5in 11.0in;
margin:1.0in 1.0in 1.0in 1.0in;}
div.WordSection1
{page:WordSection1;}
--></style></head><body lang=EN-US link="#0563C1" vlink="#954F72"><div class=WordSection1><p class=MsoNormal>**************************************************<o:p></o:p></p><p class=MsoNormal> The Thirteenth NASA Formal Methods Symposium<o:p></o:p></p><p class=MsoNormal> https://shemesh.larc.nasa.gov/nfm2021/ <o:p></o:p></p><p class=MsoNormal> 24-28 May 2021<o:p></o:p></p><p class=MsoNormal> Norfolk, VA, USA<o:p></o:p></p><p class=MsoNormal>**************************************************<o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>The symposium will be held in an in-person/virtual hybrid format in Norfolk, VA, USA,<o:p></o:p></p><p class=MsoNormal>possibly transitioning to fully virtual depending on the COVID-19 situation.<o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>Theme of the Symposium:<o:p></o:p></p><p class=MsoNormal>-----------------------<o:p></o:p></p><p class=MsoNormal>The widespread use and increasing complexity of mission-critical and safety-critical systems<o:p></o:p></p><p class=MsoNormal>at NASA and in the aerospace industry require advanced techniques that address these systems'<o:p></o:p></p><p class=MsoNormal>specification, design, verification, validation, and certification requirements.<o:p></o:p></p><p class=MsoNormal>The NASA Formal Methods Symposium (NFM) is a forum to foster collaboration between theoreticians<o:p></o:p></p><p class=MsoNormal>and practitioners from NASA, academia, and industry. NFM's goals are to identify challenges and<o:p></o:p></p><p class=MsoNormal>to provide solutions for achieving assurance for such critical systems.<o:p></o:p></p><p class=MsoNormal>New developments and emerging applications like autonomous software for Unmanned Aerial Systems (UAS),<o:p></o:p></p><p class=MsoNormal>UAS Traffic Management (UTM), advanced separation assurance algorithms for aircraft, and the need for<o:p></o:p></p><p class=MsoNormal>system-wide fault detection, diagnosis, and prognostics provide new challenges for system<o:p></o:p></p><p class=MsoNormal>specification, development, and verification approaches. Similar challenges need to be addressed<o:p></o:p></p><p class=MsoNormal>during development and deployment of on-board software for both spacecraft and ground systems.<o:p></o:p></p><p class=MsoNormal>The focus of the symposium will be on formal techniques and other approaches for software assurance,<o:p></o:p></p><p class=MsoNormal>including their theory, current capabilities and limitations, as well as their potential application<o:p></o:p></p><p class=MsoNormal>to aerospace, robotics, and other NASA-relevant safety-critical systems during all stages of the<o:p></o:p></p><p class=MsoNormal>software life-cycle.<o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>The NASA Formal Methods Symposium is an annual event organized by the NASA Formal Methods (NFM)<o:p></o:p></p><p class=MsoNormal>Research Group, comprised of researchers spanning six NASA centers. NFM2021 is being organized by<o:p></o:p></p><p class=MsoNormal>the NASA Langley Formal Methods Team.<o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>Topics of Interest:<o:p></o:p></p><p class=MsoNormal>-------------------<o:p></o:p></p><p class=MsoNormal>We encourage submissions on cross-cutting approaches that bring together formal methods and<o:p></o:p></p><p class=MsoNormal>techniques from other domains such as probabilistic reasoning, machine learning, control theory,<o:p></o:p></p><p class=MsoNormal>robotics, and quantum computing among others.<o:p></o:p></p><p class=MsoNormal>Topics of interest include, but are not limited to, the following aspects of formal methods:<o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>- Advances in formal methods:<o:p></o:p></p><p class=MsoNormal> - Formal verification, model checking, and static analysis techniques<o:p></o:p></p><p class=MsoNormal> - Theorem proving: advances in interactive and automated theorem proving (SAT, SMT, etc.)<o:p></o:p></p><p class=MsoNormal> - Program and specification synthesis, code transformation and generation<o:p></o:p></p><p class=MsoNormal> - Run-time verification<o:p></o:p></p><p class=MsoNormal> - Techniques and algorithms for scaling formal methods<o:p></o:p></p><p class=MsoNormal> - Test case generation<o:p></o:p></p><p class=MsoNormal> - Design for verification and correct-by-design techniques<o:p></o:p></p><p class=MsoNormal> - Requirements generation, specification, and validation<o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>- Integration of formal methods techniques:<o:p></o:p></p><p class=MsoNormal> - Use of machine learning techniques in formal methods<o:p></o:p></p><p class=MsoNormal> - Integration of formal methods into software engineering practices <o:p></o:p></p><p class=MsoNormal> - Integration of diverse formal methods techniques<o:p></o:p></p><p class=MsoNormal> - Combination of formal methods with simulation and analysis techniques<o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>- Formal methods in practice<o:p></o:p></p><p class=MsoNormal> - Experience report of application of formal methods in industry<o:p></o:p></p><p class=MsoNormal> - Use of formal methods in education<o:p></o:p></p><p class=MsoNormal> - Verification of machine learning techniques<o:p></o:p></p><p class=MsoNormal> - Applications of formal methods in the development of:<o:p></o:p></p><p class=MsoNormal> - autonomous systems,<o:p></o:p></p><p class=MsoNormal> - safety-critical systems,<o:p></o:p></p><p class=MsoNormal> - concurrent and distributed systems,<o:p></o:p></p><p class=MsoNormal> - cyber-physical, embedded, and hybrid systems<o:p></o:p></p><p class=MsoNormal> - fault-detection, diagnostics, and prognostics systems<o:p></o:p></p><p class=MsoNormal> - human-machine interaction analysis<o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>Important Dates:<o:p></o:p></p><p class=MsoNormal>----------------<o:p></o:p></p><p class=MsoNormal>Abstract Submission: 27 November 2020<o:p></o:p></p><p class=MsoNormal>Paper Submission: 4 December 2020<o:p></o:p></p><p class=MsoNormal>Paper Notifications: 19 February 2021<o:p></o:p></p><p class=MsoNormal>Camera-ready Papers: 19 March 2021<o:p></o:p></p><p class=MsoNormal>Symposium: 24-28 May 2021<o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>Submission Details:<o:p></o:p></p><p class=MsoNormal>-------------------<o:p></o:p></p><p class=MsoNormal>There are two categories of submissions:<o:p></o:p></p><p class=MsoNormal>1. Regular papers describing fully developed work and complete results (maximum 15 pages);<o:p></o:p></p><p class=MsoNormal>2. Short papers on tools, experience reports, or work in progress with preliminary results (maximum 6 pages).<o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>The submitted papers should not exceed 15 pages for regular papers and 6 pages for short papers,<o:p></o:p></p><p class=MsoNormal>including tables and figures, but excluding bibliography and clearly marked appendices.<o:p></o:p></p><p class=MsoNormal>The papers should be self-contained, as appendices will not be included in the published proceedings.<o:p></o:p></p><p class=MsoNormal>In addition to appendices, authors are encouraged to make available any other supplementary material<o:p></o:p></p><p class=MsoNormal>supporting the claims made in the paper, such as proof scripts or experimental data, as the<o:p></o:p></p><p class=MsoNormal>availability and reproducibility of these artifacts may be considered by reviewers in scoring.<o:p></o:p></p><p class=MsoNormal>All papers must be in English and describe original work that has not been published or submitted elsewhere.<o:p></o:p></p><p class=MsoNormal>All submissions will be reviewed by at least three members of the Program Committee in a single-blind<o:p></o:p></p><p class=MsoNormal>reviewing format.<o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>Papers will appear in the Formal Methods subline of Springer's Lecture Notes in Computer Science (LNCS) and must use LNCS<o:p></o:p></p><p class=MsoNormal>style formatting (https://www.springer.com/gp/computer-science/lncs/conference-proceedings-guidelines).<o:p></o:p></p><p class=MsoNormal>Papers must be submitted in PDF format at the EasyChair submission site:<o:p></o:p></p><p class=MsoNormal>https://easychair.org/conferences/?conf=nfm2021<o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>Authors of selected best papers will be invited to submit an extended version to a special issue in<o:p></o:p></p><p class=MsoNormal>Springer's Innovations in Systems and Software Engineering: A NASA Journal (https://www.springer.com/journal/11334).<o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>Organizers:<o:p></o:p></p><p class=MsoNormal>-----------<o:p></o:p></p><p class=MsoNormal>• Cesar Munoz, NASA, USA (General Co-Chair)<o:p></o:p></p><p class=MsoNormal>• Ivan Perez, National Institute of Aerospace, USA (General Co-Chair)<o:p></o:p></p><p class=MsoNormal>• Aaron Dutle, NASA, USA (PC Co-Chair)<o:p></o:p></p><p class=MsoNormal>• Mariano Moscato, National Institute of Aerospace, USA (PC Co-Chair)<o:p></o:p></p><p class=MsoNormal>• Laura Titolo, National Institute of Aerospace, USA (PC Co-Chair)<o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>Program Committee:<o:p></o:p></p><p class=MsoNormal>------------------<o:p></o:p></p><p class=MsoNormal>Erika Abraham, RWTH Aachen University, Germany<o:p></o:p></p><p class=MsoNormal>Mauricio Ayala-Rincon, Universidade de Brasilia, Brazil<o:p></o:p></p><p class=MsoNormal>Julia Badger, NASA, USA<o:p></o:p></p><p class=MsoNormal>Nikolaj Bjorner, Microsoft Research, USA<o:p></o:p></p><p class=MsoNormal>Jasmin Blanchette, Vrije Universiteit Amsterdam, The Netherlands<o:p></o:p></p><p class=MsoNormal>Sylvie Boldo, INRIA, France<o:p></o:p></p><p class=MsoNormal>Alessandro Cimatti, Fondazione Bruno Kessler, Italy<o:p></o:p></p><p class=MsoNormal>Misty Davies, NASA, USA<o:p></o:p></p><p class=MsoNormal>Gilles Dowek, INRIA / ENS Paris-Saclay, France<o:p></o:p></p><p class=MsoNormal>Catherine Dubois, ENSIIE-Samovar, France<o:p></o:p></p><p class=MsoNormal>Alexandre Duret-Lutz, LRDE/EPITA, France<o:p></o:p></p><p class=MsoNormal>Gabriel Ebner, Vienna University of Technology, Austria <o:p></o:p></p><p class=MsoNormal>Marco Feliu, National Institute of Aerospace, USA<o:p></o:p></p><p class=MsoNormal>Jean-Christophe Filliatre, CNRS, France<o:p></o:p></p><p class=MsoNormal>Pierre-Loic Garoche, ENAC, France<o:p></o:p></p><p class=MsoNormal>Alwyn Goodloe, NASA, USA<o:p></o:p></p><p class=MsoNormal>John Harrison, Amazon Web Services, USA<o:p></o:p></p><p class=MsoNormal>Klaus Havelund, NASA Jet Propulsion Laboratory, USA<o:p></o:p></p><p class=MsoNormal>Marieke Huisman, University of Twente, The Netherlands<o:p></o:p></p><p class=MsoNormal>Brian Jalaian, ARL / Virginia Tech, USA<o:p></o:p></p><p class=MsoNormal>Susmit Jha, SRI International, USA<o:p></o:p></p><p class=MsoNormal>Michael Lowry, NASA, USA<o:p></o:p></p><p class=MsoNormal>Panagiotis Manolios, Northeastern University, USA<o:p></o:p></p><p class=MsoNormal>Paolo Masci, National Institute of Aerospace, USA<o:p></o:p></p><p class=MsoNormal>Anastasia Mavridou, SGT Inc. / NASA Ames Research Center, USA<o:p></o:p></p><p class=MsoNormal>Stefan Mitsch, Carnegie Mellon University, USA<o:p></o:p></p><p class=MsoNormal>Yannick Moy, AdaCore / INRIA, France<o:p></o:p></p><p class=MsoNormal>Natasha Neogi, NASA, USA<o:p></o:p></p><p class=MsoNormal>Laura Panizo, University of Malaga, Spain<o:p></o:p></p><p class=MsoNormal>Corina Pasareanu, CMU / NASA Ames Research Center, USA<o:p></o:p></p><p class=MsoNormal>Zvonimir Rakamaric, University of Utah, USA<o:p></o:p></p><p class=MsoNormal>Camilo Rocha, Pontificia Universidad Javeriana Cali, Colombia<o:p></o:p></p><p class=MsoNormal>Nicolas Rosner, Amazon Web Services, USA<o:p></o:p></p><p class=MsoNormal>Kristin-Yvonne Rozier, Iowa State University, USA<o:p></o:p></p><p class=MsoNormal>Cristina Seceleanu, Malardalen University, Sweden<o:p></o:p></p><p class=MsoNormal>Natarajan Shankar, SRI International, USA<o:p></o:p></p><p class=MsoNormal>Johann Schumann, SGT Inc./NASA Ames Research Center, USA<o:p></o:p></p><p class=MsoNormal>Tanner Slagel, NASA, USA<o:p></o:p></p><p class=MsoNormal>Marielle Stoelinga, University of Twente, The Netherlands<o:p></o:p></p><p class=MsoNormal>Cesare Tinelli, University of Iowa, USA<o:p></o:p></p><p class=MsoNormal>Caterina Urban, INRIA, France<o:p></o:p></p><p class=MsoNormal>Virginie Wiels, ONERA / DTIM, France<o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>Registration:<o:p></o:p></p><p class=MsoNormal>-------------<o:p></o:p></p><p class=MsoNormal>Registration is required and free of charge.<o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>Contact:<o:p></o:p></p><p class=MsoNormal>--------<o:p></o:p></p><p class=MsoNormal>Email: nfm2021 [at] easychair [dot] org<o:p></o:p></p><p class=MsoNormal>Web: https://shemesh.larc.nasa.gov/nfm2021/<o:p></o:p></p></div></body></html>