NASA Formal Methods : 14th International Symposium, NFM 2022, Pasadena, CA, USA, May 24-27, 2022, Proceedings (Lecture Notes in Computer Science)

個数:

NASA Formal Methods : 14th International Symposium, NFM 2022, Pasadena, CA, USA, May 24-27, 2022, Proceedings (Lecture Notes in Computer Science)

  • 提携先の海外書籍取次会社に在庫がございます。通常3週間で発送いたします。
    重要ご説明事項
    1. 納期遅延や、ご入手不能となる場合が若干ございます。
    2. 複数冊ご注文の場合、分割発送となる場合がございます。
    3. 美品のご指定は承りかねます。

    ●3Dセキュア導入とクレジットカードによるお支払いについて
  • 【入荷遅延について】
    世界情勢の影響により、海外からお取り寄せとなる洋書・洋古書の入荷が、表示している標準的な納期よりも遅延する場合がございます。
    おそれいりますが、あらかじめご了承くださいますようお願い申し上げます。
  • ◆画像の表紙や帯等は実物とは異なる場合があります。
  • ◆ウェブストアでの洋書販売価格は、弊社店舗等での販売価格とは異なります。
    また、洋書販売価格は、ご注文確定時点での日本円価格となります。
    ご注文確定後に、同じ洋書の販売価格が変動しても、それは反映されません。
  • 製本 Paperback:紙装版/ペーパーバック版/ページ数 828 p.
  • 言語 ENG
  • 商品コード 9783031067723

Full Description

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. 

 

Contents

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.

最近チェックした商品