NASA formal methods : 14th international symposium, NFM 2022, Pasadena, CA, USA, May 24-27, 2022 : proceedings

This book constitutes the proceedings of the 14th International Symposium on NASA Formal Methods, NFM 2022, held in Pasadena, USA, during May 24-27, 2022. The 33 full and 6 short papers presented in this volume were carefully reviewed and selected from 118 submissions. The volume also contains 6 invited papers. The papers deal with advances in formal methods, formal methods techniques, and formal methods in practice. The focus on topics such as interactive and automated theorem proving; SMT and SAT solving; model checking; use of machine learning and probabilistic reasoning in formal methods; formal methods and graphical modeling languages such as SysML or UML; usability of formal method tools and application in industry, etc. Preface Organization Abstracts of Invited Tutorials Total Functional Programming in Idris: A Tutorial • Edwin Brady The Lean 4 Theorem Proverand Programming Language: A Tutorial • Leonardo de Moura and Sebastian Ullrich Formally Reasoning about Distributed Systems using P • Ankush Desai Contents Invited Keynotes Formal Methods for Trusted Space Autonomy: Boon or Bane? • Steve A. Chien An Essence of Domain Engineering: A Basis for Trustworthy Aeronautics and Space Software • Dines Bjørner Concept Design Moves • Daniel Jackson Automating Program Transformation with Coccinelle • Julia Lawall and Gilles Muller The Prusti Project: Formal Verification for Rust • Vytautas Astrauskas, Aurel Bílý, Jonáš Fiala, Zachary Grannan, Christoph Matheja, Peter Müller, Federico Poli, and Alexander J. Summers Reachability Analysis for Cyber-Physical Systems: Are We There Yet? • Xin Chen and Sriram Sankaranarayanan Regular Submissions Towards Better Test Coverage: Merging Unit Tests for Autonomous Systemsy • Josefine B. Graebener, Apurva Badithela, and Richard M. Murray Quantification of Battery Depletion Risk Made Efficient • Holger Hermanns and Gilles Nies Hierarchical Contract-Based Synthesis for Assurance Cases • Timothy E. Wang, Zamira Daw, Pierluigi Nuzzo, and Alessandro Pinto Verified Probabilistic Policies for Deep Reinforcement Learning • Edoardo Bacci and David Parker NNLander-VeriF: A Neural Network Formal Verification Framework for Vision-Based Autonomous Aircraft Landing • Ulices Santa Cruz and Yasser Shoukry The Black-Box Simplex Architecture for Runtime Assurance of Autonomous CPS • Usama Mehmood, Sanaz Sheikhi, Stanley Bak, Scott A. Smolka, and Scott D. Stoller Case Studies for Computing Density of Reachable States for Safe Autonomous Motion Planning • Yue Meng, Zeng Qiu, Md Tawhid Bin Waez, and Chuchu Fan Towards Refactoring FRETish Requirements • Marie Farrell, Matt Luckcuck, Oisín Sheridan, and Rosemary Monahan Neural Network Compression of ACAS Xu Early Prototype Is Unsafe: Closed-Loop Verification Through Quantized State Backreachability • Stanley Bak and Hoang-Dung Tran ZoPE: A Fast Optimizer for ReLU Networks with Low-Dimensional Inputs • Christopher A. Strong, Sydney M. Katz, Anthony L. Corso, and Mykel J. Kochenderfer Permutation Invariance of Deep Neural Networks with ReLUs • Diganta Mukhopadhyay, Kumar Madhukar, and Mandayam Srivas Configurable Benchmarks for C Model Checkers • Xaver Fink, Philipp Berger, and Joost-Pieter Katoen Assume-Guarantee Reasoning with Scheduled Components • Cong Liu, Junaid Babar, Isaac Amundson, Karl Hoech, Darren Cofer, and Eric Mercer Stateful Black-Box Fuzzing of Bluetooth Devices Using Automata Learning • Andrea Pferscher and Bernhard K. Aichernig From Verified Scala to STIX File System Embedded Code Using Stainless • Jad Hamza, Simon Felix, Viktor Kunčak, Ivo Nussbaumer, and Filip Schramka On the Termination of Borrow Checking in Featherweight Rust • Étienne Payet, David J. Pearce, and Fausto Spoto More Programming Than Programming: Teaching Formal Methods in a Software Engineering Programme • James Noble, David Streader, Isaac Oscar Gariano, and Miniruwani Samarakoon Zone Extrapolations in Parametric Timed Automata • Johan Arcile and Étienne André Exemplifying Parametric Timed Specifications over Signals with Bounded Behavior • Étienne André, Masaki Waga, Natuski Urabe, and Ichiro Hasuo Timed Automata Learning via SMT Solving • Martin Tappler, Bernhard K. Aichernig, and Florian Lorber Asynchronous Composition of Local Interface LTL Properties • Alberto Bombardelli and Stefano Tonetta Elucidation and Analysis of Specification Patterns in Aerospace System Telemetry • Zachary Luppen, Michael Jacks, Nathan Baughman, Muhamed Stilic, Ryan Nasers, Benjamin Hertz, James Cutler, Dae-Young Lee,and Kristin Yvonne Rozier Robust Computation Tree Logic • Satya Prakash Nayak, Daniel Neider, Rajarshi Roy, and Martin Zimmermann On-the-Fly Model Checking with Neural MCTS • Ruiyang Xu and Karl Lieberherr Requirements-Driven Model Checking and Test Generation for Comprehensive Verification • Devesh Bhatt, Hao Ren, Anitha Murugesan, Jason Biatek, Srivatsan Varadarajan, and Natarajan Shankar Operational Annotations: A New Method for Sequential Program Verification • Paul C. Attie Towards Formal Verification of HotStuff-Based Byzantine Fault Tolerant Consensus in Agda • Harold Carr, Christa Jenkins, Mark Moir, Victor Cacciari Miraldo, and Lisandra Silva DSV: Disassembly Soundness Validation Without Assuming a Ground Truth • Xiaoxin An, Freek Verbeek, and Binoy Ravindran Probabilistic Hyperproperties with Rewards • Oyendrila Dobe, Lukas Wilke, Erika Ábrahám, Ezio Bartocci, and Borzoo Bonakdarpour Hypercontracts • Inigo Incer, Albert Benveniste, Alberto Sangiovanni-Vincentelli, and Sanjit A. Seshia Monitorability of Expressive Verdicts • Felipe Gorostiaga and César Sánchez BDDs Strike Back: Efficient Analysis of Static and Dynamic Fault Trees • Daniel Basgöze, Matthias Volk, Joost-Pieter Katoen, Shahid Khan, and Marielle Stoelinga Approximate Translation from Floating-Point to Real-Interval Arithmetic • Daisuke Ishii, Takashi Tomita, and Toshiaki Aoki Synthesis of Optimal Defenses for System Architecture Design Model in MaxSMT • Baoluo Meng, Arjun Viswanathan, William Smith, Abha Moitra, Kit Siu, and Michael Durling Certified Computation of Nondeterministic Limits • Michal Konečný, Sewon Park, and Holger Thies The Power of Disjoint Support Decompositions in Decision Diagrams • Lieuwe Vinkhuijzen and Alfons Laarman Incremental Transitive Closure for Zonal Abstract Domain • Kenny Ballou and Elena Sherman Proof Mate: An Interactive Proof Helper for PVS (Tool Paper) • Paolo Masci and Aaron Dutle Runtime Verification Triggers Real-Time, Autonomous Fault Recovery on the CySat-I • Alexis Aurandt, Phillip H. Jones, and Kristin Yvonne Rozier Author Index