LEADER 00816nam0-22002891i-450- 001 990000995660403321 035 $a000099566 035 $aFED01000099566 035 $a(Aleph)000099566FED01 035 $a000099566 100 $a20000920d1970----km-y0itay50------ba 101 0 $aeng 200 1 $aQuanta$eEssays in Theoretical Physics dedicated to Gregor Wentzel$fPeter Freund, Nambu Goebel 210 $aOxford$cCambridge University Press$d1970 610 0 $aMeccanica quantistica 676 $a530.12 700 1$aFreund,$bPeter$046963 702 1$aGoebel,$bNambu 702 1$aWentzel,$bGregor$f<1898- > 801 0$aIT$bUNINA$gRICA$2UNIMARC 901 $aBK 912 $a990000995660403321 952 $a22-151$b11324$fFI1 959 $aFI1 996 $aQuanta$9354182 997 $aUNINA DB $aING01 LEADER 04522nam 22007095 450 001 996664549803316 005 20250608130235.0 010 $a3-031-93706-6 024 7 $a10.1007/978-3-031-93706-4 035 $a(CKB)39239631500041 035 $a(MiAaPQ)EBC32149955 035 $a(Au-PeEL)EBL32149955 035 $a(DE-He213)978-3-031-93706-4 035 $a(EXLCZ)9939239631500041 100 $a20250608d2025 u| 0 101 0 $aeng 135 $aur||||||||||| 181 $ctxt$2rdacontent 182 $cc$2rdamedia 183 $acr$2rdacarrier 200 10$aNASA Formal Methods $e17th International Symposium, NFM 2025, Williamsburg, VA, USA, June 11?13, 2025, Proceedings /$fedited by Aaron Dutle, Laura Humphrey, Laura Titolo 205 $a1st ed. 2025. 210 1$aCham :$cSpringer Nature Switzerland :$cImprint: Springer,$d2025. 215 $a1 online resource (820 pages) 225 1 $aLecture Notes in Computer Science,$x1611-3349 ;$v15682 311 08$a3-031-93705-8 327 $aEnforcing MAVLink Safety & Security Properties Via Refined Multiparty Session Types -- Process-Algebraic Semantics for Verifying Intelligent Robotic Control Software -- Towards a Safe, Verified Runtime Monitor for Embedded Systems: R2U2 in Embedded Rust -- Verification of an Anti-Unification Algorithm in PVS -- Strong Structural Bounds for MaxSAT: The Fine Details of Using Neuromorphic and Quantum Hardware Accelerators -- Vellvm: Formalizing the Informal LLVM (Experience Report) -- Eliminating flakiness: deterministic control for validating nondeterministic Asmeta specifications -- Mode-based Reactive Synthesis -- Reusable Formal Verification of DAG-based Consensus Protocols -- A Streamlined, Formal Approach to Requirements-based Testing -- Formally Proving Invariant Systemic Properties of Control Programs Using Ghost Code and Integral Quadratic Constraints -- Querying Labeled Time Series Data with Scenario Programs -- Formal Verification as a Service: A CERN-GSI Case Study -- Formal Verification of Composite Field Multipliers for Information-Theoretically Secure Radio Communication in Spacecraft Control -- Rare Event Simulation for Stochastic Hybrid Systems using Symbolic Importance Functions -- Algorithmic Analysis of Event-B in Rewriting Logic -- HyTwin: A Formal Semantics for Digital Twin Interventions in ICS Based on Time-to-Violation -- Language Partitioning for Mission-time Linear Temporal Logic -- Visualizing Temporal Interval Hierarchies -- Mechanized RS274 semantics for additive manufacturing -- An SMT Formalization of Mixed-Precision Matrix Multiplication (Modeling Three Generations of Tensor Cores) -- TRACE: Toolkit for Requirements Analysis, Capture, and Elicitation -- Extending Dynamic Logics with First-Class Relational Reasoning -- Automata Size Reduction by Procedure Finding. 330 $aThis book constitutes the proceedings of the 17th International Symposium on NASA Formal Methods, NFM 2025, held in Hampton Roads, VA, USA in June 2025. The 20 full papers and 4 short papers presented in the proceedings were carefully reviewed and selected from 74 submissions. They focus on formal techniques for software and system assurance for applications in space, aviation, robotics, and other NASA-relevant critical systems. . 410 0$aLecture Notes in Computer Science,$x1611-3349 ;$v15682 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 700 $aDutle$b Aaron$01825717 701 $aHumphrey$b Laura$01825718 701 $aTitolo$b Laura$01429403 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a996664549803316 996 $aNASA Formal Methods$94393595 997 $aUNISA