NASA Formal Methods

Invited Keynotes.- Formal Methods for Trusted Space Autonomy: Boon or Bane.- An Essence of Domain Engineering - A Basis for Trustworthy Aeronautics and Space Software.- Concept Design Moves.- Automating Program Transformation with Coccinelle.- The Prusti Project: Formal Verification for Rust.- Summers Reachability Analysis for Cyber-Physical Systems: Are we there yet.- Regular Submissions.- Towards Better Test Coverage: Merging Unit Tests for Autonomous Systems.- Quantification of Battery Depletion Risk Made Efficient.- Hierarchical Contract-based Synthesis for Assurance Cases.- Verified Probabilistic Policies for Deep Reinforcement Learning.- NNLander-VeriF: A Neural Network Formal Verification Framework for Vision-Based Autonomous Aircraft Landing.- The Black-Box Simplex Architecture for Runtime Assurance of Autonomous CPS.- Case Studies for Computing Density of Reachable States for Safe Autonomous Motion Planning.- Towards Refactoring FRETish Requirements.- Neural Network Compression of ACAS Xu Early Prototype is Unsafe: Closed-Loop Verification through Quantized State Backreachability.- ZoPE: A Fast Optimizer for ReLU Networks with Low-Dimensional Inputs.- Permutation Invariance of Deep Neural Networks with ReLUs.- Configurable Benchmarks for C Model Checkers.- AssumeGuarantee Reasoning with Scheduled Components.- Stateful Black-Box Fuzzing of Bluetooth Devices Using Automata Learning.- From Verified Scala to STIX File System Embedded Code using Stainless.- On the Termination of Borrow Checking in Featherweight Rust.- Programming Than Programming: Teaching Formal Methods in a Software Engineering Programme.- Zone Extrapolations in Parametric Timed Automata.- Exemplifying Parametric Timed Specifications over Signals with Bounded Behavior.- Timed Automata Learning via SMT Solving.- Asynchronous Composition of Local Interface LTL Properties.- Elucidation and Analysis of Specification Patterns in Aerospace System Telemetry.- Robust Computation