Cantitate/Preț
Produs

NASA Formal Methods: 14th International Symposium, NFM 2022, Pasadena, CA, USA, May 24–27, 2022, Proceedings: Lecture Notes in Computer Science, cartea 13260

Editat de Jyotirmoy V. Deshmukh, Klaus Havelund, Ivan Perez
en Limba Engleză Paperback – 20 mai 2022
This book constitutes the proceedings of the 14th International Symposium on NASA Formal Methods, NFM 2022, held in Pasadena, USA, during May 24-27, 2022.
The 33 full and 6 short papers presented in this volume were carefully reviewed and selected from 118submissions. The volume also contains 6 invited papers.
The papers deal with advances in formal methods, formal methods techniques, and formal methods in practice. The focus on topics such as interactive and automated theorem proving; SMT and SAT solving; model checking; use of machine learning and probabilistic reasoning in formal methods; formal methods and graphical modeling languages such as SysML or UML; usability of formal method tools and application in industry, etc. 
 
Citește tot Restrânge

Din seria Lecture Notes in Computer Science

Preț: 82652 lei

Preț vechi: 103315 lei
-20% Nou

Puncte Express: 1240

Preț estimativ în valută:
15816 16702$ 13162£

Carte tipărită la comandă

Livrare economică 13-27 ianuarie 25

Preluare comenzi: 021 569.72.76

Specificații

ISBN-13: 9783031067723
ISBN-10: 303106772X
Pagini: 828
Ilustrații: XXII, 828 p. 219 illus., 168 illus. in color.
Dimensiuni: 155 x 235 mm
Greutate: 1.17 kg
Ediția:1st ed. 2022
Editura: Springer International Publishing
Colecția Springer
Seria Lecture Notes in Computer Science

Locul publicării:Cham, Switzerland

Cuprins

Invited Keynotes.- Formal Methods for Trusted Space Autonomy: Boon or Bane.- An Essence of Domain Engineering - A Basis for Trustworthy Aeronautics and Space Software.- Concept Design Moves.- Automating Program Transformation with Coccinelle.- The Prusti Project: Formal Verification for Rust.- Summers Reachability Analysis for Cyber-Physical Systems: Are we there yet.- Regular Submissions.- Towards Better Test Coverage: Merging Unit Tests for Autonomous Systems.- Quantification of Battery Depletion Risk Made Efficient.- Hierarchical Contract-based Synthesis for Assurance Cases.- Verified Probabilistic Policies for Deep Reinforcement Learning.- NNLander-VeriF: A Neural Network Formal Verification Framework for Vision-Based Autonomous Aircraft Landing.- The Black-Box Simplex Architecture for Runtime Assurance of Autonomous CPS.- Case Studies for Computing Density of Reachable States for Safe Autonomous Motion Planning.- Towards Refactoring FRETish Requirements.- Neural Network Compression of ACAS Xu Early Prototype is Unsafe: Closed-Loop Verification through Quantized State Backreachability.- ZoPE: A Fast Optimizer for ReLU Networks with Low-Dimensional Inputs.- Permutation Invariance of Deep Neural Networks with ReLUs.- Configurable Benchmarks for C Model Checkers.- AssumeGuarantee Reasoning with Scheduled Components.- Stateful Black-Box Fuzzing of Bluetooth Devices Using Automata Learning.- From Verified Scala to STIX File System Embedded Code using Stainless.- On the Termination of Borrow Checking in Featherweight Rust.- Programming Than Programming: Teaching Formal Methods in a Software Engineering Programme.- Zone Extrapolations in Parametric Timed Automata.- Exemplifying Parametric Timed Specifications over Signals with Bounded Behavior.- Timed Automata Learning via SMT Solving.- Asynchronous Composition of Local Interface LTL Properties.- Elucidation and Analysis of Specification Patterns in Aerospace System Telemetry.- Robust Computation TreeLogic.- On the-Fly Model Checking with Neural MCTS.- Checking and Test Generation for Comprehensive Verification.- Operational Annotations: a New Method for Sequential Program Verification.- Byzantine Fault Tolerant Consensus in Agda.- DSV: Disassembly Soundness Validation without Assuming a Ground Truth.- Probabilistic Hyperproperties with Rewards.- Hypercontracts.- Monitorability of Expressive Verdicts.- BDDs Strike Back: Efficient Analysis of Static and Dynamic Fault Trees.- Approximate Translation from Floating-Point to Real-Interval Arithmetic.- Synthesis of Optimal Defenses for System Architecture Design Model in MaxSMT.- Certified Computation of Nondeterministic Limits.- The Power of Disjoint Support Decompositions in Decision Diagrams.- Incremental Transitive Closure for Zonal Abstract Domain.- Proof Mate: an Interactive Proof Helper for PVS.- Runtime Verification Triggers.- Real-time, Autonomous Fault Recovery on the CySat-I.