NFM 2022 - CALL FOR PAPERS The 14th NASA Formal Methods Symposium https://nfm2022.caltech.edu May 24-27, 2022 Pasadena, California, USA *** EXTENDED SUBMISSION DEADLINE: January 10, 2022 *** The symposium is planned to be held in person at California Institute of Technology, but potentially transitioning to fully virtual if the COVID situation persists. Virtual presentations will be possible even if the conference is held in-person. The symposium has NO registration fee for presenting and attending. IMPORTANT DATES (Any time On Earth) - Abstract Submission: January 10, 2022 *** extended *** - Paper Submission: January 10, 2022 *** extended *** - Paper Notifications: March 10, 2022 - Camera-ready Papers: March 28, 2022 - Symposium: May 24-27, 2022 THEME OF SYMPOSIUM The widespread use and increasing complexity of mission-critical and safety-critical systems at NASA and in the aerospace industry requires 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. The focus of the symposium will be on formal/rigorous techniques for software assurance, including their theory, current capabilities and limitations, as well as their potential application to aerospace during all stages of the software life-cycle. The NASA Formal Methods Symposium is an annual event organized by the NASA Formal Methods (NFM) Research Group, composed of researchers spanning six NASA centers. The organization of NFM 2022 is being led by NASA's Jet Propulsion Laboratory (JPL), located in Pasadena, California. INVITED TALKS AND TUTORIALS - Dines Bjoerner, Technical University of Denmark, Denmark - Edwin Brady, University of St. Andrews, UK - Steve Chien, NASA JPL, USA - Ankush Desai, Amazon Web Services, USA - Daniel Jackson, MIT, USA - Julia Lawall, INRIA Paris, France - Anastasia Mavridou, KBR Inc / NASA Ames Research Center, USA - Leonardo De Moura, Microsoft Research, USA - Sriram Sankaranarayanan, University of Colorado Boulder, USA - Alex Summers, University of British Columbia, Canada - Emina Torlak, University of Washington, USA TOPICS ON INTEREST Topics of interest include, but are not limited to, the following aspects of formal methods: Advances in formal methods - Interactive and automated theorem proving - SMT and SAT solving - Model checking - Static analysis - Runtime verification - Automated testing - Specification languages, textual and graphical - Refinement - Code synthesis - Design for verification and correct-by-design techniques - Requirements specification and analysis Integration of formal methods techniques - Integration of diverse formal methods techniques - Use of machine learning and probabilistic reasoning techniques in formal methods - Integration of formal methods into software engineering practices. - Combination of formal methods with simulation and analysis techniques - Formal methods and fault tolerance, resilient computing, and self healing systems - Formal methods and graphical modeling languages such as SysML, UML, MATLAB/Simulink - Formal methods and autonomy, e.g., verification of systems and languages for planning and scheduling (PDDL, Plexil, etc.), self-sufficient systems, and fault-tolerant systems. Formal methods in practice - Experience reports of application of formal methods on real systems, such as autonomous systems, safety-critical systems, concurrent and distributed systems, cyber-physical, embedded, and hybrid systems, fault-detection, diagnostics, and prognostics systems, and human-machine interaction analysis. - Use of formal methods in systems engineering (including hardware components) - Use of formal methods in education - Reports on negative results in the development and the application for formal methods in practice. - Usability of formal method tools, and their infusion into industrial contexts. - Challenge problems for future reference by the formal methods community. The formulation of these papers can range from plain English description of a problem over formal specifications, to specific implementations in a programming language. NASA OPEN SOURCE Courageous authors, who want to delve in open source software being applied in real NASA missions, and find possible connections to and applications of Formal Methods, are invited to visit the open source repositories for the following two frameworks for programming flight software: - F' (https://nasa.github.io/fprime/) - cFS (https://cfs.gsfc.nasa.gov/) SUBMISSIONS There are two categories of submissions: - Regular papers describing fully developed work and complete results (maximum 15 pages, excluding references); - Short papers on tools, experience reports, or work in progress with preliminary results (maximum 6 pages, excluding references). Additional appendices can be submitted as supplementary material for reviewing purposes. They will not be included in the proceedings. All papers must be in English and describe original work that has not been published. All submissions will be reviewed by at least three members of the Program Committee. Reviewing is Single-blind. We encourage authors to focus on readability of their submissions. Papers will appear in the Formal Methods subline of Springer's Lecture Notes in Computer Science (LNCS) and must use LNCS style formatting (https://www.springer.com/gp/computer-science/lncs/conference-proceedings-guidelines). Papers must be submitted in PDF format at the EasyChair submission site: https://easychair.org/conferences/?conf=nfm2022. Authors of selected best papers will be invited to submit an extended version to a special issue in Springer's Innovations in Systems and Software Engineering: A NASA Journal (https://www.springer.com/journal/11334). ARTIFACTS Authors are encouraged, but not strictly required, to refer to artifacts (via urls in the paper) that support the conclusions of their work (if allowed by their institutions). Artifacts may contain software, mechanized proofs, benchmarks, examples, case studies and data sets. Artifacts will be evaluated by the Program Committee together with the paper. ORGANIZERS PC chairs - Klaus Havelund, NASA JPL, USA - Jyo Deshmukh, USC, USA - Ivan Perez, NIA, USA Application Advisors - Robert Bocchino, NASA JPL, USA - John Day, NASA JPL, USA - Maged Elasaar, NASA JPL, USA - Amalaye Oyake, Blue Origin, USA - Nicolas Rouquette, NASA JPL, USA - Vandi Verma, NASA JPL, USA Application advisors advise the PC chairs to ensure a strong connection to the problems facing NASA. Local Organizer - Richard Murray, Caltech, USA Scientific Advisor - Mani Chandy, Caltech, USA Program Committee - Aaron Dutle, NASA Langley, USA - Alessandro Cimatti, Fondazione Bruno Kessler, Italy - Alwyn Goodloe, NASA Langley, USA - Anastasia Mavridou, SGT Inc. / NASA Ames, USA - Anne-Kathrin Schmuck, Max-Planck-Institute for Software Systems, Germany - Arie Gurfinkel, University of Waterloo, Canada - Bardh Hoxha, Toyota Research Institute North America, USA - Bernd Finkbeiner, CISPA Helmholtz Center for Information Security, Germany - Betty H.C. Cheng, Michigan State University, USA - Borzoo Bonakdarpour, Michigan State University, USA - Carolyn Talcott, SRI International, USA - Chuchu Fan, MIT, USA - Constance Heitmeyer, Naval Research Laboratory, USA - Corina Pasareanu, CMU, NASA Ames, KBR, USA - Cristina Seceleanu, Mälardalen University, Sweden - Dejan Nickovic, Austrian Institute of Technology AIT, Austria - Dirk Beyer, LMU Munich, Germany - Doron Peled, Bar Ilan University, Israel - Erika Abraham, RWTH Aachen University, Germany - Ewen Denney, NASA Ames, USA - Gerard Holzmann, Nimble Research, USA - Giles Reger, Amazon Web Services, UK - Guy Katz, Hebrew University of Jerusalem, Israel - Huafeng Yu, TOYOTA InfoTechnology Center USA, USA - Jean-Christophe Filliatre, CNRS, France - Johann Schumann, NASA Ames, USA - John Day, NASA JPL, USA - Julia Badger, NASA Houston, USA - Julien Signoles, CEA LIST, France - Kerianne Hobbs, Air Force Research Laboratory, USA - Kim Larsen, Aalborg University, Denmark - Kristin Yvonne Rozier, Iowa State University, USA - Leonardo Mariani, University of Milano Bicocca, Italy - Lu Feng, University of Virginia, USA - Marcel Verhoef, European Space Agency, The Netherlands - Marie Farrell, Maynooth University, Ireland - Marieke Huisman, University of Twente, The Netherlands - Marielle Stoelinga, University of Twente, The Netherlands - Martin Feather, NASA JPL, USA - Martin Leucker, University of Luebeck, Germany - Michael Lowry, NASA Ames, USA - Misty Davies, NASA Ames, USA - Natalia Alexandria, NASA Langley, USA - Natasha Neogi, NASA Langley, USA - Nicolas Rouquette, NASA JPL, USA - Nikos Arechiga, Toyota Research Institute, USA - Oleg Sokolsky, University of Pennsylvania, USA - Pavithra Prabhakar, Kansas State University - Rajeev Joshi, Amazon Web Services, USA - Rudiger Ehlers, Clausthal University of Technology, Germany - Stanley Bak, Stony Brook University, USA - Susmit Jha, SRI International, USA - Sylvie Boldo, INRIA, France - Vandi Verma, NASA JPL, USA - Willem Visser, Amazon Web Services, USA - Yasser Shoukry, University of California Irvine, USA - Ylies Falcone, University Grenoble Alpes, France CONTACT Email: nfm2022 [at] easychair [dot] org Last update: 2022-01-18