This book constitutes the proceedings of the 13th International Symposium on NASA Formal Methods, NFM 2021, held virtually in May 2021.
The 21 full and 3 short papers presented in this volume were carefully reviewed and selected from 66 submissions. The papers aim to identify challenges and provide solutions to achieve assurance in mission-critical and safety-critical systems. Examples of such systems include advanced separation assurance algorithms for aircraft, next-generation air transportation, autonomous rendezvous and docking of spacecraft, on-board software for unmanned aerial systems (UAS), UAS traffic management, autonomous robots, and systems for fault detection, diagnosis, and prognostics.
Inhaltsverzeichnis
Balancing Wind and Batteries: Towards Predictive Verification of Smart Grids. - nnenum: Verification of ReLU Neural Networks with Optimized Abstraction Refinement. - Minimum-Violation Traffic Management for Urban Air Mobility. - Integrating Formal Verification and Assurance: An Inspection Rover Case Study. - Towards verifying SHA256 in OpenSSL with the Software Analysis Workbench. - Polygon Merge: A Geometric Algorithm Verified Using PVS. - Program Sketching using Lifted Analysis for Numerical Program Families. - Specification Decomposition for Reactive Synthesis. - On Symmetry and Quantification: A New Approach to Verify Distributed Protocols. - Integrating Runtime Verification into a Sounding Rocket Control System. - Verification of Functional Correctness of Code Diversi cation Techniques. - Scalable Reliability Analysis by Lazy Verification. - Robustifying Controller Specifications of Cyber-Physical Systems Against Perceptual Uncertainty. - Good fences make good neighbors: Using formally verified safe trajectories to design a predictive geofence algorithm. - Online Shielding for Stochastic Systems. - Verification of Eventual Consensus in Synod Using a Failure-Aware Actor Model. - An Infrastructure for Faithful Execution of Remote Attestation Protocols. - Verifying min-plus Computations with Coq. - Efficient Verification of Optimized Code: Correct High-speed X25519. - A formal proof of the Lax equivalence theorem for finite difference schemes. - Recursive Variable-Length State Compression for Multi-Core Software Model Checking. - Runtime Verification of Generalized Test Tables. - Quasi-Equal Clock Reduction On-the-Fly. - On the Effectiveness of Signal Rescaling in Hybrid System Falsification.
