LEADER 04963nam 22007575 450 001 9910728938503321 005 20230602122957.0 010 $a3-031-33170-2 024 7 $a10.1007/978-3-031-33170-1 035 $a(MiAaPQ)EBC30564802 035 $a(Au-PeEL)EBL30564802 035 $a(OCoLC)1381446174 035 $a(DE-He213)978-3-031-33170-1 035 $a(BIP)090943805 035 $a(PPN)272259403 035 $a(CKB)26821655900041 035 $a(EXLCZ)9926821655900041 100 $a20230602d2023 u| 0 101 0 $aeng 135 $aurcnu|||||||| 181 $ctxt$2rdacontent 182 $cc$2rdamedia 183 $acr$2rdacarrier 200 10$aNASA Formal Methods $e15th International Symposium, NFM 2023, Houston, TX, USA, May 16?18, 2023, Proceedings /$fedited by Kristin Yvonne Rozier, Swarat Chaudhuri 205 $a1st ed. 2023. 210 1$aCham :$cSpringer Nature Switzerland :$cImprint: Springer,$d2023. 215 $a1 online resource (508 pages) 225 1 $aLecture Notes in Computer Science,$x1611-3349 ;$v13903 311 08$aPrint version: Rozier, Kristin Yvonne NASA Formal Methods Cham : Springer,c2023 9783031331695 327 $aNon-linear Activation Functions -- Open and Closed-Loop Neural Network Verification using Polynomial Zonotopes -- Verifying Attention Robustness of Deep Neural Networks against Semantic Perturbations -- Formalizing Piecewise Affne Activation Functions of Neural Networks in Coq -- Verifying an Aircraft Collision Avoidance Neural Network with Marabou -- Strategy Synthesis in Markov Decision Processes Under Limited Sampling Access -- Learning Symbolic Timed Models from Concrete Timed Data -- Reward Shaping from Hybrid Systems Models in Reinforcement Learning -- Conservative Safety Monitors of Stochastic Dynamical Systems -- Code-level Formal Verification of Ellipsoidal Invariant Sets for Linear Parameter-Varying Systems -- Reasoning with Metric Temporal Logic and Resettable Skewed Clocks -- Formal Guarantees for Centralized Multi-Agent Synthesis with Spatial Constraints via Mixed-Integer Quadratic Programming -- A Framework for Policy Based Negotiation -- Rewrite-Based Decomposition of Signal Temporal Logic Specifications -- Quantitative Verification and Strategy Synthesis for BDI Agents -- Multi-Objective Task Assignment and Multiagent Planning with Hybrid GPU-CPU Acceleration -- Reasoning over Test Specifications using Assume-Guarantee Contracts -- Formally Proved Memory Controllers: From the Standards to Silicon -- Formalising Liveness Properties in Event-B with the Reflexive EB4EB Framework -- Formalized High Level Synthesis with Applications to Cryptographic Hardware -- From Natural Language Requirements to the Verification of Programmable Logic Controllers: Integrating FRET into PLCverif -- Automata-Based Software Model Checking of Hyperproperties -- Condition Synthesis Realizability via Constrained Horn Clauses -- A Toolkit for Automated Testing of Dafny -- Verified ALL(*) Parsing with Semantic Actions and Dynamic Input Validation -- Subtropical Satisfiability for SMT Solving -- A Linear Weight Transfer Rule for Local Search -- 1.1 : Zero-suppressed Decision Diagrams in External Memory -- Satisfiability of Non-Linear Transcendental Arithmetic as a Certificate Search Problem. 330 $aThis book constitutes the proceedings of the 15th International Symposium on NASA Formal Methods, NFM 2023, held in Houston, Texas, USA, during May 16-18, 2023. The 26 full and 3 short papers presented in this volume were carefully reviewed and selected from 75 submissions. The papers deal with advances in formal methods, formal methods techniques, and formal methods in practice. . 410 0$aLecture Notes in Computer Science,$x1611-3349 ;$v13903 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 610 $aMathematics 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 $a004.0151 676 $a004.0151 700 $aRozier$b Kristin Yvonne$01367076 701 $aChaudhuri$b Swarat$01367077 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a9910728938503321 996 $aNASA Formal Methods$93389816 997 $aUNINA