001436747 000__ 04955cam\a2200649\i\4500 001436747 001__ 1436747 001436747 003__ OCoLC 001436747 005__ 20230309004111.0 001436747 006__ m\\\\\o\\d\\\\\\\\ 001436747 007__ cr\cn\nnnunnun 001436747 008__ 210522s2021\\\\sz\\\\\\o\\\\\101\0\eng\d 001436747 019__ $$a1252703805 001436747 020__ $$a9783030763848$$q(electronic bk.) 001436747 020__ $$a3030763846$$q(electronic bk.) 001436747 020__ $$z3030763838 001436747 020__ $$z9783030763831 001436747 0247_ $$a10.1007/978-3-030-76384-8$$2doi 001436747 035__ $$aSP(OCoLC)1252427294 001436747 040__ $$aEBLCP$$beng$$erda$$epn$$cEBLCP$$dGW5XE$$dYDX$$dOCLCO$$dOCLCF$$dOCLCO$$dOCLCQ$$dCOM$$dOCLCO$$dTXI$$dOCLCQ 001436747 049__ $$aISEA 001436747 050_4 $$aQA76.9.F67 001436747 08204 $$a004.01/51$$223 001436747 1112_ $$aNFM (Symposium)$$n(13th :$$d2021 :$$cOnline) 001436747 24510 $$aNASA formal methods :$$b13th International Symposium, NFM 2021, virtual event, May 24-28, 2021 : proceedings /$$cAaron Dutle, Mariano M. Moscato, Laura Titolo, César A. Muñoz, Ivan Perez (eds.). 001436747 2463_ $$aNFM 2021 001436747 264_1 $$aCham :$$bSpringer,$$c[2021] 001436747 264_4 $$c©2021 001436747 300__ $$a1 online resource (416 pages) 001436747 336__ $$atext$$btxt$$2rdacontent 001436747 337__ $$acomputer$$bc$$2rdamedia 001436747 338__ $$aonline resource$$bcr$$2rdacarrier 001436747 4901_ $$aLecture notes in computer science ;$$v12673 001436747 500__ $$aInternational conference proceedings. 001436747 500__ $$aIncludes author index. 001436747 5050_ $$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. 001436747 506__ $$aAccess limited to authorized users. 001436747 520__ $$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. 001436747 588__ $$aDescription based on print version record. 001436747 650_0 $$aFormal methods (Computer science)$$vCongresses. 001436747 650_6 $$aMéthodes formelles (Informatique)$$vCongrès. 001436747 655_7 $$aConference papers and proceedings.$$2fast$$0(OCoLC)fst01423772 001436747 655_7 $$aConference papers and proceedings.$$2lcgft 001436747 655_7 $$aActes de congrès.$$2rvmgf 001436747 655_0 $$aElectronic books. 001436747 7001_ $$aDutle, Aaron Michael,$$eeditor. 001436747 7001_ $$aMoscato, Mariano M.,$$eeditor. 001436747 7001_ $$aTitolo, Laura,$$eeditor. 001436747 7001_ $$aMuñoz, César A.,$$d1968-$$eeditor. 001436747 7001_ $$aPerez, Ivan$$c(Research scientist),$$eeditor. 001436747 77608 $$iPrint version:$$aDutle, Aaron.$$tNASA Formal Methods.$$dCham : Springer International Publishing AG, ©2021$$z9783030763831 001436747 830_0 $$aLecture notes in computer science ;$$v12673. 001436747 852__ $$bebk 001436747 85640 $$3Springer Nature$$uhttps://univsouthin.idm.oclc.org/login?url=https://link.springer.com/10.1007/978-3-030-76384-8$$zOnline Access$$91397441.1 001436747 909CO $$ooai:library.usi.edu:1436747$$pGLOBAL_SET 001436747 980__ $$aBIB 001436747 980__ $$aEBOOK 001436747 982__ $$aEbook 001436747 983__ $$aOnline 001436747 994__ $$a92$$bISE