東華大學圖書館 |

Language: English

Help

回圖書館首頁

手機版館藏查詢

Back

Switch To: Labeled | MARC Mode | ISBD

Nasa formal methods = 17th Internati...

NFM (Conference) (2025 :)

Linked to FindBook

Google Book

Amazon

博客來

Nasa formal methods = 17th International Symposium, NFM 2025, Williamsburg, VA, USA, June 11-13, 2025 : proceedings /

Record Type:	Electronic resources : Monograph/item
Title/Author:	Nasa formal methods/ edited by Aaron Dutle, Laura Humphrey, Laura Titolo.
Reminder of title:	17th International Symposium, NFM 2025, Williamsburg, VA, USA, June 11-13, 2025 : proceedings /
remainder title:	NFM 2025
other author:	Dutle, Aaron.
corporate name:	NFM (Conference)
Published:	Cham :Springer Nature Switzerland : : 2025.,
Description:	xiii, 442 p. :ill. (some col.), digital ;24 cm.
[NT 15003449]:	Enforcing 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.
Contained By:	Springer Nature eBook
Subject:	Formal methods (Computer science) - Congresses. -
Online resource:	https://doi.org/10.1007/978-3-031-93706-4
ISBN:	9783031937064

Nasa formal methods = 17th International Symposium, NFM 2025, Williamsburg, VA, USA, June 11-13, 2025 : proceedings /
Nasa formal methods17th International Symposium, NFM 2025, Williamsburg, VA, USA, June 11-13, 2025 : proceedings /[electronic resource] :NFM 2025edited by Aaron Dutle, Laura Humphrey, Laura Titolo. - Cham :Springer Nature Switzerland :2025. - xiii, 442 p. :ill. (some col.), digital ;24 cm. - Lecture notes in computer science,156821611-3349 ;. - Lecture notes in computer science ;15682..

Enforcing 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.

This 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.

ISBN: 9783031937064

Standard No.: 10.1007/978-3-031-93706-4doiSubjects--Topical Terms:

622707
Formal methods (Computer science)
--Congresses.

LC Class. No.: QA76.9.F67

Dewey Class. No.: 004.0151

Nasa formal methods = 17th International Symposium, NFM 2025, Williamsburg, VA, USA, June 11-13, 2025 : proceedings /
LDR:03476nmm a2200361 a 4500 001 2413309
003 DE-He213
005 20250608130235.0
006 m d
007 cr nn 008maaau
008 260205s2025 sz s 0 eng d
020 $a 9783031937064 $q (electronic bk.)
020 $a 9783031937057 $q (paper)
024 7 $a 10.1007/978-3-031-93706-4 $2 doi
035 $a 978-3-031-93706-4
040 $a GP $c GP
041 0 $a eng
050 4 $a QA76.9.F67
072 7 $a UMZ $2 bicssc
072 7 $a COM051230 $2 bisacsh
072 7 $a UMZ $2 thema
082 0 4 $a 004.0151 $2 23
090 $a QA76.9.F67 $b N575 2025
111 2 $a NFM (Conference) $n (17th : $d 2025 : $c Williamsburg, Va.) $3 3789264
245 1 0 $a Nasa formal methods $h [electronic resource] : $b 17th International Symposium, NFM 2025, Williamsburg, VA, USA, June 11-13, 2025 : proceedings / $c edited by Aaron Dutle, Laura Humphrey, Laura Titolo.
246 3 $a NFM 2025
260 $a Cham : $b Springer Nature Switzerland : $b Imprint: Springer, $c 2025.
300 $a xiii, 442 p. : $b ill. (some col.), digital ; $c 24 cm.
338 $a online resource $b cr $2 rdacarrier
490 1 $a Lecture notes in computer science, $x 1611-3349 ; $v 15682
505 0 $a Enforcing 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.
520 $a This 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.
650 0 $a Formal methods (Computer science) $v Congresses. $3 622707
650 1 4 $a Software Engineering. $3 890874
650 2 4 $a Theory of Computation. $3 892514
650 2 4 $a Computer Engineering and Networks. $3 3538504
650 2 4 $a Artificial Intelligence. $3 769149
650 2 4 $a Computer Modelling. $3 3538541
700 1 $a Dutle, Aaron. $3 3308045
700 1 $a Humphrey, Laura. $3 3789265
700 1 $a Titolo, Laura. $3 3666154
710 2 $a SpringerLink (Online service) $3 836513
773 0 $t Springer Nature eBook
830 0 $a Lecture notes in computer science ; $v 15682. $3 3789266
856 4 0 $u https://doi.org/10.1007/978-3-031-93706-4
950 $a Computer Science (SpringerNature-11645)