000			04763nam a22006135i 4500
001			978-3-031-33170-1
003			DE-He213
005			20240423125517.0
007			cr nn 008mamaa
008			230602s2023 sz | s |||| 0|eng d
020			_a9783031331701 _9978-3-031-33170-1
024	7		_a10.1007/978-3-031-33170-1 _2doi
050		4	_aQA76.758
072		7	_aUMZ _2bicssc
072		7	_aCOM051230 _2bisacsh
072		7	_aUMZ _2thema
082	0	4	_a005.1 _223
245	1	0	_aNASA Formal Methods _h[electronic resource] : _b15th International Symposium, NFM 2023, Houston, TX, USA, May 16–18, 2023, Proceedings / _cedited by Kristin Yvonne Rozier, Swarat Chaudhuri.
250			_a1st ed. 2023.
264		1	_aCham : _bSpringer Nature Switzerland : _bImprint: Springer, _c2023.
300			_aXXIII, 490 p. 149 illus., 89 illus. in color. _bonline resource.
336			_atext _btxt _2rdacontent
337			_acomputer _bc _2rdamedia
338			_aonline resource _bcr _2rdacarrier
347			_atext file _bPDF _2rda
490	1		_aLecture Notes in Computer Science, _x1611-3349 ; _v13903
505	0		_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.
520			_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. .
650		0	_aSoftware engineering.
650		0	_aComputer science.
650		0	_aComputer engineering.
650		0	_aComputer networks .
650		0	_aArtificial intelligence.
650		0	_aComputer simulation.
650	1	4	_aSoftware Engineering.
650	2	4	_aTheory of Computation.
650	2	4	_aComputer Engineering and Networks.
650	2	4	_aArtificial Intelligence.
650	2	4	_aComputer Modelling.
700	1		_aRozier, Kristin Yvonne. _eeditor. _4edt _4http://id.loc.gov/vocabulary/relators/edt
700	1		_aChaudhuri, Swarat. _eeditor. _4edt _4http://id.loc.gov/vocabulary/relators/edt
710	2		_aSpringerLink (Online service)
773	0		_tSpringer Nature eBook
776	0	8	_iPrinted edition: _z9783031331695
776	0	8	_iPrinted edition: _z9783031331718
830		0	_aLecture Notes in Computer Science, _x1611-3349 ; _v13903
856	4	0	_uhttps://doi.org/10.1007/978-3-031-33170-1
912			_aZDB-2-SCS
912			_aZDB-2-SXCS
912			_aZDB-2-LNC
942			_cSPRINGER
999			_c178725 _d178725