NASA Formal Methods 12th International Symposium, NFM 2020, Moffett Field, CA, USA, May 11–15, 2020, Proceedings

This book constitutes the proceedings of the 12th International Symposium on NASA Formal Methods, NFM 2020, held in Moffett Field, CA, USA, in May 2020.*

The 20 full and 5 short papers presented in this volume were carefully reviewed and selected from 62 submissions. The papers are organized in the following topical sections:  learning and formal synthesis; formal methods for DNNs; high assurance systems; requirement specification and testing; validation and solvers; solvers and program analysis; verification and times systems; autonomy and other applications; and hybrid and cyber-physical systems.

*The conference was held virtually due to the COVID-19 pandemic.

Learning and Formal Synthesis.- From Passive to Active: Learning Timed Automata Efficiently.- Generating Correct-by-Construction Distributed Implementations from Formal Maude Designs.- Parameter Synthesis and Robustness Analysis of Rule-Based Models.- Formal Methods for DNNs.- PaRoT: A Practical Framework for Robust Deep Neural Network Training.- Simplifying Neural Networks using Formal Verification.- High Assurance Systems.- Neural Simplex Architecture.- Strengthening Deterministic Policies for POMDPs.- Benchmarking Software Model Checkers on Automotive Code.- Requirement Specification and Testing.- Automated Requirements-Based Testing of Black-Box Reactive Systems.- Formal Verification of Parallel Prefix Sum.- Specification Quality Metrics Based on Mutation and Inductive Incremental Model Checking.- Validation and Solvers.- A Validation Methodology for OCaml-to-PVS Translation.- On the Usefulness of Clause Strengthening in Parallel SAT Solving.- Solvers and Program Analysis.- Verifying a Solver for Linear Mixed Integer Arithmetic in Isabelle/HOL*.- Constraint Caching Revisited.- Per-Location Simulation.- Verification and Timed Systems.- Sampling Distributed Schedules for Resilient Space Communication.- Model Checking Timed Hyperproperties in Discrete-Time Systems.- Verifying Band Convergence for Sampled Control Systems.- Autonomy and Other Applications.- Heterogeneous Verification of an Autonomous Curiosity Rover.- Run-Time Assurance for Learning-Enabled Systems.- hpnmg: A CC++ Tool for Model Checking Hybrid Petri Nets with General Transitions.- Hybrid and Cyber-Physical Systems.- A Transformation of Hybrid Petri Nets with Stochastic Firings into a Subclass of Stochastic Hybrid Automata.- Constraining Counterexamples in Hybrid System Falsification: Penalty-Based Approaches.- Falsification of Cyber-Physical Systems with Constrained Signal Spaces.