<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" style='word-wrap:break-word'><div class=WordSection1><p class=MsoNormal>**************************************************<o:p></o:p></p><p class=MsoNormal> Final Call for Papers -- Extended Deadline<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> May 24-28, 2021<o:p></o:p></p><p class=MsoNormal> Virtual / 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>Currently, the symposium is planned to be held in an in-person/virtual hybrid<o:p></o:p></p><p class=MsoNormal>format in Norfolk, VA, USA, highly likely transitioning to fully virtual if the<o:p></o:p></p><p class=MsoNormal>COVID-19 situation persists. Virtual presentation of papers will be possible<o:p></o:p></p><p class=MsoNormal>even if the conference is also held in-person.<o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>Important Dates (Extend Deadline):<o:p></o:p></p><p class=MsoNormal>-----------------------------<o:p></o:p></p><p class=MsoNormal>Abstract Submission: December 7, 2020 (extended)<o:p></o:p></p><p class=MsoNormal>Paper Submission: December 14, 2020 (extended)<o:p></o:p></p><p class=MsoNormal>Paper Notifications: February 19, 2021<o:p></o:p></p><p class=MsoNormal>Camera-ready Papers: March 19, 2021<o:p></o:p></p><p class=MsoNormal>Symposium: May 24-28, 2021<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<o:p></o:p></p><p class=MsoNormal>safety-critical systems at NASA and in the aerospace industry require<o:p></o:p></p><p class=MsoNormal>advanced techniques that address these systems' specification, design,<o:p></o:p></p><p class=MsoNormal>verification, validation, and certification requirements. The NASA<o:p></o:p></p><p class=MsoNormal>Formal Methods Symposium (NFM) is a forum to foster collaboration<o:p></o:p></p><p class=MsoNormal>between theoreticians and practitioners from NASA, academia, and<o:p></o:p></p><p class=MsoNormal>industry. NFM's goals are to identify challenges and to provide<o:p></o:p></p><p class=MsoNormal>solutions for achieving assurance for such critical systems. New<o:p></o:p></p><p class=MsoNormal>developments and emerging applications like autonomous software for<o:p></o:p></p><p class=MsoNormal>Unmanned Aerial Systems (UAS), UAS Traffic Management (UTM), advanced<o:p></o:p></p><p class=MsoNormal>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<o:p></o:p></p><p class=MsoNormal>challenges for system specification, development, and verification<o:p></o:p></p><p class=MsoNormal>approaches. Similar challenges need to be addressed during development<o:p></o:p></p><p class=MsoNormal>and deployment of on-board software for both spacecraft and ground<o:p></o:p></p><p class=MsoNormal>systems. The focus of the symposium will be on formal techniques and<o:p></o:p></p><p class=MsoNormal>other approaches for software assurance, including their theory,<o:p></o:p></p><p class=MsoNormal>current capabilities and limitations, as well as their potential<o:p></o:p></p><p class=MsoNormal>application to aerospace, robotics, and other NASA-relevant<o:p></o:p></p><p class=MsoNormal>safety-critical systems during all stages of the 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<o:p></o:p></p><p class=MsoNormal>NASA Formal Methods (NFM) Research Group, comprised of researchers<o:p></o:p></p><p class=MsoNormal>spanning six NASA centers. NFM2021 is being organized by the NASA<o:p></o:p></p><p class=MsoNormal>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<o:p></o:p></p><p class=MsoNormal>together formal methods and techniques from other domains such as<o:p></o:p></p><p class=MsoNormal>probabilistic reasoning, machine learning, control theory, robotics,<o:p></o:p></p><p class=MsoNormal>and quantum computing among others. Topics of interest include, but<o:p></o:p></p><p class=MsoNormal>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<o:p></o:p></p><p class=MsoNormal> 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>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<o:p></o:p></p><p class=MsoNormal> (maximum 15 pages);<o:p></o:p></p><p class=MsoNormal>2. Short papers on tools, experience reports, or work in progress with<o:p></o:p></p><p class=MsoNormal> 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<o:p></o:p></p><p class=MsoNormal>6 pages for short papers, including tables and figures, but excluding<o:p></o:p></p><p class=MsoNormal>bibliography and clearly marked appendices. The papers should be<o:p></o:p></p><p class=MsoNormal>self-contained, as appendices will not be included in the published<o:p></o:p></p><p class=MsoNormal>proceedings. In addition to appendices, authors are encouraged to<o:p></o:p></p><p class=MsoNormal>make available any other supplementary material supporting the claims<o:p></o:p></p><p class=MsoNormal>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<o:p></o:p></p><p class=MsoNormal>by reviewers in scoring. All papers must be in English and describe<o:p></o:p></p><p class=MsoNormal>original work that has not been published or submitted elsewhere. All<o:p></o:p></p><p class=MsoNormal>submissions will be reviewed by at least three members of the Program<o:p></o:p></p><p class=MsoNormal>Committee in a single-blind 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<o:p></o:p></p><p class=MsoNormal>Notes in Computer Science (LNCS) and must use LNCS style formatting<o:p></o:p></p><p class=MsoNormal>(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<o:p></o:p></p><p class=MsoNormal>site: 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<o:p></o:p></p><p class=MsoNormal>version to a special issue in Springer's Innovations in Systems and<o:p></o:p></p><p class=MsoNormal>Software Engineering: A NASA Journal<o:p></o:p></p><p class=MsoNormal>(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><p class=MsoNormal><o:p> </o:p></p></div></body></html>