LEADER 04748nam 22007095 450 001 9910483828703321 005 20250414104349.0 010 $a3-030-76384-6 024 7 $a10.1007/978-3-030-76384-8 035 $a(CKB)4100000011930420 035 $a(DE-He213)978-3-030-76384-8 035 $a(MiAaPQ)EBC6627555 035 $a(Au-PeEL)EBL6627555 035 $a(OCoLC)1252427294 035 $a(PPN)255881479 035 $a(EXLCZ)994100000011930420 100 $a20210516d2021 u| 0 101 0 $aeng 135 $aurnn|008mamaa 181 $ctxt$2rdacontent 182 $cc$2rdamedia 183 $acr$2rdacarrier 200 10$aNASA Formal Methods $e13th International Symposium, NFM 2021, Virtual Event, May 24?28, 2021, Proceedings /$fedited by Aaron Dutle, Mariano M. Moscato, Laura Titolo, César A. Muñoz, Ivan Perez 205 $a1st ed. 2021. 210 1$aCham :$cSpringer International Publishing :$cImprint: Springer,$d2021. 215 $a1 online resource (XVI, 402 p. 133 illus., 80 illus. in color.) 225 1 $aProgramming and Software Engineering,$x2945-9168 ;$v12673 311 08$a3-030-76383-8 327 $aBalancing 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. 330 $aThis 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. 410 0$aProgramming and Software Engineering,$x2945-9168 ;$v12673 606 $aSoftware engineering 606 $aComputer science 606 $aComputer engineering 606 $aComputer networks 606 $aArtificial intelligence 606 $aComputer simulation 606 $aSoftware Engineering 606 $aTheory of Computation 606 $aComputer Engineering and Networks 606 $aArtificial Intelligence 606 $aComputer Modelling 615 0$aSoftware engineering. 615 0$aComputer science. 615 0$aComputer engineering. 615 0$aComputer networks. 615 0$aArtificial intelligence. 615 0$aComputer simulation. 615 14$aSoftware Engineering. 615 24$aTheory of Computation. 615 24$aComputer Engineering and Networks. 615 24$aArtificial Intelligence. 615 24$aComputer Modelling. 676 $a005.1 702 $aDutle$b Aaron 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a9910483828703321 996 $aNASA Formal Methods$92860155 997 $aUNINA