دانلود کتاب NASA Formal Methods: 15th International Symposium, NFM 2023, Houston, TX, USA, May 16–18, 2023, Proceedings

فهرست مطالب :

Preface
Organization
Invited Talks
Design Automation for Verified AI-Based Autonomy
Formal Guarantees for Autonomous Operation of Human Spacecraft
Proof-Based Heuristics for Quantified Invariant Synthesis
Contents
Verification of LSTM Neural Networks with Non-linear Activation Functions
1 Introduction
2 Background
2.1 LSTM Architecture
3 Approach to LSTM Verification
3.1 Encoding LSTMs into iSAT
4 Case Study
4.1 NGSIM
4.2 Satellite Collision Detection
5 Conclusion
References
Open- and Closed-Loop Neural Network Verification Using Polynomial Zonotopes
1 Introduction
1.1 State of the Art
1.2 Overview
1.3 Notation
2 Preliminaries
3 Image Enclosure
3.1 Activation Function Approximation
3.2 Bounding the Approximation Error
4 Neural Network Controlled Systems
5 Operations on Polynomial Zonotopes
6 Numerical Examples
7 Conclusion
References
Verifying Attention Robustness of Deep Neural Networks Against Semantic Perturbations
1 Introduction
2 Overview
3 Problem Formulation
4 Geometric Boundary Search (GBS)
4.1 Encoding Semantic Perturbations
4.2 Traversing Activation Regions
4.3 Calculating Attention Inconsistency
4.4 Verifying CR/MR and AR/IR
5 Experimental Evaluation
6 Related Work
7 Conclusion and Future Work
H Appendix
H.1 Linearity of Activation Regions
H.2 Connectivity of Activation Regions
H.3 Hierarchy of Activation Regions
H.4 Linear Programming on an Activation Region
H.5 Full Encoding Semantic Perturbations
H.6 Images Used for Our Experiments
H.7 An Example of Lemma 1
H.8 Algorithm BFS
H.9 Details of Experimental Results
References
Formalizing Piecewise Affine Activation Functions of Neural Networks in Coq
1 Introduction
2 Preliminaries
2.1 Piecewise Affine Topology
2.2 Neural Networks
2.3 Interactive Theorem Prover Coq & Library Coquelicot
3 Formalization of Piecewise Affine Functions in Coq
3.1 Inductive Definition of PWA Functions
3.2 Example: Rectified Linear Unit Activation Function
4 Verified Transformation of a Neural Network to a pwa Function
4.1 Neural Network Model in Coq
4.2 Composition of PWA Functions
4.3 Concatenation: Layers of Neural Networks as PWA Functions
4.4 Transforming a Neural Network into a pwa Function
5 Discussion
References
Verifying an Aircraft Collision Avoidance Neural Network with Marabou
1 Introduction
2 Aircraft Collision Avoidance Neural Network
3 Verifying Minimum Separation Distance
4 Robustness Analysis
5 Specific Scenarios
6 Conclusion and Future Work
References
Strategy Synthesis in Markov Decision Processes Under Limited Sampling Access
1 Introduction
2 Preliminaries
3 Interval MDP Reinforcement Learning
3.1 Generating IMDPs from Sampled Gray-Box MDPs
3.2 IMDP-Based PAC Reinforcement Learning
4 Learning Under Limited Sampling Access
4.1 Lower Confidence Bound Sampling
4.2 Action Scoping
5 Implementation and Evaluation
5.1 Experiment Setup
5.2 Sampling Methods (RQ1)
5.3 Impact of Scoping (RQ2)
5.4 Further Examples
6 Concluding Remarks
References
Learning Symbolic Timed Models from Concrete Timed Data
1 Introduction
2 Preliminaries
3 Trace Database
4 From Concrete Traces to Symbolic Runs
5 Application in Model Learning Scenarios
6 Related Work
7 Conclusion
References
Reward Shaping from Hybrid Systems Models in Reinforcement Learning
1 Introduction
2 Background
2.1 Differential Dynamic Logic
2.2 ModelPlex
2.3 Reinforcement Learning and Reward Shaping
3 Related Work
4 Rewards from Hybrid Systems Models
4.1 Quantitative Interpretation of ModelPlex Formulas
4.2 Logical Constraint Reward
4.3 Reward Scaling
4.4 Potential-Based Logical Constraint Reward
5 Evaluation
6 Conclusion
References
Conservative Safety Monitors of Stochastic Dynamical Systems
1 Introduction
2 Related Work
3 Background
4 Problem Statement
5 Overall Approach
5.1 Design Time
5.2 Runtime
6 Conservatism Guarantees
7 Case Study
7.1 Water Tanks
7.2 Results
8 Conclusion
References
Code-Level Formal Verification of Ellipsoidal Invariant Sets for Linear Parameter-Varying Systems
1 Introduction
2 Affine LPV Systems and Ellipsoidal Invariant Sets
3 Frama-C Setup
3.1 C Code of System Dynamics
3.2 Invariant Set ACSL Annotation
3.3 Contract-Based Verification
4 Validating Contracts: Real Model
5 Validating Contracts: Float Model
5.1 Issues with Deductive Methods and the Floating-Point Model
5.2 Bounding Numerical Errors
5.3 Error Hyper-Rectangle Approach
5.4 Error Ball Approach
6 Conclusion
References
Reasoning with Metric Temporal Logic and Resettable Skewed Clocks
1 Introduction
2 Motivating Example
2.1 Semantics with Resettable Skewed Clocks
2.2 Compositional Reasoning Example
3 Related Work
4 First-Order LTL over Discrete or Super-Dense Time
4.1 Discrete and Super-Dense Time
4.2 Linear Temporal Logic
5 MTL with Skewed Clocks and Resets
6 Encoding and Verification
6.1 LTL-min-max Definition and Rewriting
6.2 LTL-min-max Discretization
6.3 LTL-min-max Discrete Encoding
7 Results
7.1 Implementation
7.2 Experimental Evaluation
8 Conclusions
References
Centralized Multi-agent Synthesis with Spatial Constraints via Mixed-Integer Quadratic Programming
1 Introduction
2 Related Work
3 Problem Formulation
3.1 Environment
3.2 Agents
3.3 Signal Temporal Logic
3.4 Problem Statement
4 Mixed Integer Programming Encodings
4.1 Agent Dynamics
4.2 Objective Satisfaction
4.3 Team Actions
4.4 Quadratic Spatial Constraint Encoding
4.5 Linear Spatial Constraints Encoding
4.6 Formula Satisfaction
5 Experiments
5.1 Case Studies
5.2 Scaling Experiments
6 Discussion
7 Conclusion
References
A Framework for Policy Based Negotiation
1 Introduction
2 Background
2.1 ISAKMP
2.2 Copland
2.3 Manifests
3 Negotiation
4 Verification
5 Example
6 Related Work
7 Conclusions and Future Work
References
Rewrite-Based Decomposition of Signal Temporal Logic Specifications
1 Introduction
2 Background and Problem Definition
3 An STL Rewriting System
3.1 Formula Rewrite DAG
4 Decomposing STL
4.1 Agent Assignments
4.2 Decomposition
4.3 Comparison of Decomposition Candidates
5 Exploring the Formula Rewrite DAG
6 Experiments and Results
6.1 CaTL Example
6.2 Case Studies
7 Conclusions
References
Quantitative Verification and Strategy Synthesis for BDI Agents
1 Introduction
2 Background
2.1 CAN
2.2 Markov Decision Processes
3 An MDP Model of CAN Semantics
3.1 Probabilistic Action Outcomes
3.2 Intention-Level Semantics
3.3 Agent-Level Semantics
3.4 Rewards
4 Implementation and Examples
4.1 Bigraph Encoding of CANm Model
4.2 Example: Smart Manufacturing
4.3 Example: Rover
4.4 Discussion
5 Related Work
6 Conclusions
A Appendix
References
Multi-objective Task Assignment and Multiagent Planning with Hybrid GPU-CPU Acceleration
1 Introduction
2 Preliminaries
3 Problem and Approach
3.1 Problem Statement
3.2 Convex Characterisation and Centralised Model
3.3 Point-Oriented Pareto Computation by Decentralised Model
4 Hybrid GPU-CPU Implementation
5 Experiments
6 Related Work
7 Conclusion
References
Reasoning over Test Specifications Using Assume-Guarantee Contracts
1 Introduction
2 Background
3 Test Structures and Tester Specifications
4 Combining Tests
5 Comparing Test Campaigns
6 Splitting Tests
7 Conclusion and Future Work
References
From the Standards to Silicon: Formally Proved Memory Controllers*-4pt
1 Introduction
2 Background
2.1 DRAM Basics
2.2 CoqDRAM
2.3 Cava
3 Coupling CoqDRAM and CavaDRAM
3.1 Controller Implementation Constraints
3.2 From CoqDRAM to CavaDRAM Implementation
4 The Equivalence Proof
5 Simulation and Synthesis
6 Related Work
7 Conclusion
References
Formalising Liveness Properties in Event-B with the Reflexive EB4EB Framework
1 Introduction
2 Event-B
3 Linear Temporal Logic
4 The EB4EB Framework
5 Trace-Based Semantics of Event-B
5.1 Semantics: Traces of Event-B Machines in EB4EB
5.2 Correctness Principle
6 A Case Study: A Read Write Machine
7 Temporal Logic Proof Rules as EB4EB POs
7.1 Liveness Properties
7.2 Deadlock Freeness P applied to the Read-Write machine
7.3 Temporal Operator Proof Rules
7.4 Existence P applied to the read write machine
8 Correctness of the Temporal Logic Properties Proof Rules
9 Related Work
10 Conclusion
References
Formalized High Level Synthesis with Applications to Cryptographic Hardware*-4pt
1 Introduction
2 Formalizing ReWire
3 Case Study: Cryptographic Hardware Verification
4 Related Work
5 Summary, Conclusions, and Future Work
A Monads, Monad Transformers, and Reactive Resumption Monads over State in Haskell
A.1 Monads in Haskell
A.2 Identity Monad
A.3 Monad Transformers in Haskell
A.4 StateT Monad Transformer
A.5 ReacT Monad Transformer
A.6 Reactive Resumption Monads over State in Haskell
References
From Natural Language Requirements to the Verification of Programmable Logic Controllers: Integrating FRET into PLCverif
1 Introduction
2 Integrating FRET into PLCverif
2.1 Limitations of Requirement Formulation in PLCverif
2.2 Realization of the New Workflow with FRET
3 Case Studies
3.1 Safety PLC Program
3.2 Standard PLC Program
4 Conclusion
References
Automata-Based Software Model Checking of Hyperproperties
1 Introduction
2 Preliminaries
2.1 Temporal Stream Logic Modulo Theories TSL(T)
3 HyperTSL Modulo Theories
4 Büchi Product Programs and TSL Model Checking
5 HyperTSL(T) Model Checking
5.1 Alternation-Free HyperTSL(T)
5.2 * * HyperTSL(T)
6 Demonstration of the Algorithm
7 Conclusions
References
Condition Synthesis Realizability via Constrained Horn Clauses
1 Introduction
2 Preliminaries
2.1 Program Safety
2.2 Constrained Horn Clauses
2.3 Program Safety as CHC Satisfiability
3 From Realizability to CHC Satisfaibility
3.1 Defining the Condition Synthesis Problem
3.2 Reducing Condition Synthesis Realizability to CHC Satisfiability
4 Realizability and the Satisfying Interpretation of S
4.1 The Role of the Resolving Function
4.2 Defining a Resolving Function
4.3 Synthesizing a Solution with a Grammar
5 Experimental Results
6 Related Work
7 Conclusion
References
A Toolkit for Automated Testing of Dafny
1 Introduction
2 Toolkit Overview
3 Unit Testing and Mocking Frameworks
4 Automated Test Generation
4.1 Custom Dafny to Boogie Translation
4.2 Trap Assertion Injection
4.3 Unit Test Generation
4.4 Limitations
5 Empirical Evaluation
5.1 Unit Testing and Coverage
5.2 Test Suite Size
6 Related Work
7 Conclusions
References
Verified ALL(*) Parsing with Semantic Actions and Dynamic Input Validation
1 Introduction
2
2.1 A Grammar for Parsing Duplicate-Free JSON
2.2 Parsing Valid and Invalid Input
3 Interpreter Correctness
3.1 Correctness Specification
3.2 Parser Correctness Theorems
4 Semantic Actions and Ambiguity
5 Semantic Predicates and Completeness
5.1 A Semantics-Aware Prediction Mechanism
5.2 A Backward-Looking Completeness Invariant
6 Performance Evaluation
7 Related Work
References
Subtropical Satisfiability for SMT Solving
1 Introduction
2 Preliminaries
2.1 SMT Solving
2.2 Subtropical Satisfiability for a Single Inequation
2.3 Subtropical Satisfiability for a Single Equation
2.4 Subtropical Satisfiability for Conjunctions of Inequations
2.5 Transformation of a QFNRA Formula into a Single Equation
3 Subtropical Satisfiability for QFNRA Formulas
3.1 Transforming a QFNRA Formula into a Single Equation
3.2 Generalizing the Subtropical Encoding to QFNRA Formulas
4 Experimental Results
4.1 Pure Subtropical Solvers
4.2 Combining Subtropical Methods with a Complete Procedure
4.3 Z3 and Cvc5
5 Conclusion
References
A Linear Weight Transfer Rule for Local Search*-4pt
1 Introduction
2 Preliminaries
3 The DDFW Algorithm
4 Solvers, Benchmarks, and Hardware
5 Modifications to the DDFW Algorithm
5.1 The Linear Weight Transfer Rule
5.2 How Much Weight Should be Given Away Initially?
5.3 The cspt Parameter
5.4 A Weighted-random Variable Selection Method
6 Empirical Evaluation
6.1 Evaluation Without Restarts
6.2 Evaluation With Restarts
6.3 Solving Hard Instances
7 Discussion and Future Work
References
Adiar 1.1
1 Introduction
2 Supporting both BDDs and ZDDs
3 Evaluation
3.1 Cost of Modularity
3.2 Experimental Evaluation
4 Conclusion and Future Work
References
Satisfiability of Non-linear Transcendental Arithmetic as a Certificate Search Problem
1 Introduction
2 Preliminaries
3 Goal
4 Method
5 Certificate Search
5.1 Points
5.2 Literals
5.3 Instantiations
5.4 Box
6 Computational Experiments
7 Related Work
8 Conclusions
References
Author Index