Formal Methods: 25th International Symposium, FM 2023, Lübeck, Germany, March 6–10, 2023, Proceedings (Lecture Notes in Computer Science)

This book constitutes the refereed proceedings of the 25th International Symposium on Formal Methods, FM 2023, which took place in Lübeck, Germany, in March 2023. The 26 full paper, 2 short papers included in this book were carefully reviewed and selected rom 95 submissions. They have been organized in topical sections as follows: SAT/SMT; Verification; Quantitative Verification; Concurrency and Memory Models; Formal Methods in AI; Safety and Reliability. The proceedings also contain 3 keynote talks and 7 papers from the industry day. Preface Organization Contents Keynotes Symbolic Computation in Automated Program Reasoning 1 Introduction 2 Symbolic Computation in Inductive Invariant Synthesis 3 Symbolic Computation in Unsolvable Loops 4 Symbolic Computation in Probabilistic Reasoning References The Next Big Thing: From Embedded Systems to Embodied Actors 1 Introduction 2 Embedded Systems 3 Embedded Systems with AI/ML 4 Embodied Actors 5 Design Challenges 5.1 Robust AI/ML 5.2 Human-Centered AI/ML 5.3 Cognitive Architectures 5.4 Uncertainty Quantification 5.5 Self-integration 5.6 Analysis 5.7 Assurance 6 Conclusion References Intelligent and Dependable Decision-Making Under Uncertainty 1 Synopsis: Robust and Dependable Artificial Intelligence 2 Research Highlights 2.1 Reliable Neural Network Controllers for Autonomous Agents 2.2 Learning Uncertainty Models 2.3 Robust Control for Dynamical Systems Under Uncertainty 2.4 Safe Deep Reinforcement Learning References SAT/SMT A Coq Formalization of Lebesgue Induction Principle and Tonelli's Theorem 1 Introduction 2 Prerequisites 2.1 The Coquelicot Library, R and Logic 2.2 Lebesgue Integration Theory 3 Lebesgue Induction Principle 4 Product Measure on a Product Space 4.1 Product -Algebra 4.2 Section of Subset 4.3 Measurability of Measure of Section 4.4 Existence and Uniqueness of the Product Measure 5 Tonelli's Theorem 5.1 Section of Function 5.2 Iterated Integral and the First Formula of Tonelli's Theorem 5.3 Change of Measure, Second Formula, and Tonelli's Theorem 6 Conclusion and Perspectives References Railway Scheduling Using Boolean Satisfiability Modulo Simulations 1 Introduction 2 Problem Overview 2.1 Example 2.2 General Problem Statement 2.3 Railway Model 2.4 Constraints 3 Theory Description 4 Encoding and Formalization 4.1 Railway Model 4.2 Schedule Constraints 5 Algorithm 6 Experimental Part 7 Conclusion References SMT Sampling via Model-Guided Approximation 1 Introduction 1.1 Motivating Example 2 Preliminaries 3 Model-Guided Approximation 4 Solving the MGA Problem 4.1 Approximating the Theory of Linear Integer Arithmetic with Non-Linear Multiplication Using the Theory of Intervals 4.2 Adding Arrays and Uninterpreted Functions 5 Sampling Using Model-Guided Approximation 6 Evaluation 6.1 Results 7 Related Work 8 Conclusion References Efficient SMT-Based Network Fault Tolerance Verification 1 Introduction 2 Motivation 3 Trailblazer 3.1 Background 3.2 Our Approach 4 Evaluation 5 Related Work 6 Conclusion References Verification I Formalising the Prevention of Microarchitectural Timing Channels by Operating Systems 1 Introduction 2 Threat Scenario 3 Modelling Channels by Elimination Strategy 3.1 Flushable Microarchitectural State 3.2 Partitionable Microarchitectural State 3.3 Interrupts and Other Directly Observed Impacts on Time 4 Formalising Time Protection 4.1 State-Dependent Policy Channels 4.2 Policy-Dependent State Observability 5 System Model of OS-Enforced Time Protection 5.1 Model Overview and Property 5.2 User Steps 5.3 OS Steps 5.4 Proof Approach 6 Related Work 7 Conclusions References Can We Communicate? Using Dynamic Logic to Verify Team Automata 1 Introduction 2 Background on Team Automata and Dynamic Logic 2.1 Component Automata and Systems 2.2 Team Automata 2.3 Dynamic Logic 3 Logical Characterisations of Communication Properties 3.1 Team Receptiveness 3.2 Logical Characterisations of Receptiveness 3.3 Team Responsiveness 3.4 Logical Characterisations of Responsiveness 4 Model Checking Communication Properties 5 Conclusions and Future Work References The ScalaFix Equation Solver 1 Introduction 2 Equation Systems 2.1 Infinite Equation Systems 2.2 Finite Equation Systems 2.3 A Use Case for Static Analysis 2.4 Infinite Equation Systems and Static Analysis 3 Widening, Narrowing and Warrowing 3.1 Automatic Determination of Combo Points 4 Equation Systems Based on Hyper-Graphs 4.1 Localized Widening 5 A High-Level Interface 6 Performance 6.1 A Simple Benchmark Using the PPL 6.2 Reaching Definitions 7 Related Work 8 Conclusion References HHLPy: Practical Verification of Hybrid Systems Using Hoare Logic 1 Introduction 2 Preliminaries 2.1 Sequential Fragment of HCSP 2.2 Translation from Simulink/Stateflow 3 Proof Rules of Hoare Logic for Hybrid Systems 3.1 Proof Rules Based on Invariants 3.2 Solution Rule 4 Verification Condition Generation 5 Labels 6 Highlighting 7 Implementation and Evaluation 7.1 Implementation 7.2 Evaluation on Simulink/Stateflow Models 7.3 Evaluation on Benchmarks from KeYmaera X 8 Related Work 9 Conclusion References Quantitative Verification symQV: Automated Symbolic Verification of Quantum Programs 1 Introduction 2 Background 2.1 Entanglement 2.2 Quantum Measurement 2.3 Running Example: Teleportation 3 The symQV Quantum Program Model 3.1 Running Example: Quantum Program Model of Teleportation 4 The symQV Verification Algorithm 4.1 Running Example: Verification of Teleportation 4.2 The symQV Over-Approximation 5 Evaluation 5.1 Implementation 5.2 Benchmark Problems and Setup 5.3 Results 6 Discussion 7 Conclusion References PFL: A Probabilistic Logic for Fault Trees 1 Introduction 2 Fault Trees: Background 3 A Probabilistic Logic to Reason About FTs 3.1 Syntax 3.2 Semantics 4 Case Study: Examples 4.1 COVID-19 FT 4.2 Oil/Gas Pipeline FT 5 LangPFL: A Domain Specific Language for PFL 6 Model Checking Algorithms 6.1 (Reduced Ordered) Binary Decision Diagrams 6.2 Translating FTs/Formulae to BDDs 6.3 Equipping BDDs with Probabilities 6.4 Algorithm 2: Model Checking PFL over a FT and a 6.5 Algorithm 3: Computing regions where -formulae are satisfied 6.6 Algorithm 4: Checking PFL -formulae over a FT for all 7 Conclusion and Future Work A Appendix: Algorithms and Additional Definitions for Layer One Formulae A.1 Translating FTs to BDDs A.2 Algorithm 5: Translating FTs/Formulae to BDDs A.3 Algorithm 6: Model Checking PFL over a FT and a b A.4 Algorithm 7: Computing all Satisfying Vectors B Appendix: Proofs B.1 Proof for Theorem 1 References Energy Büchi Problems 1 Introduction 2 Energy Büchi Problems in Finite Weighted Automata 3 Energy Büchi Problems for Weighted Timed Automata 4 Implementation 5 Benchmarks 6 Conclusion References QMaude: Quantitative Specification and Verification in Rewriting Logic 1 Introduction 2 Preliminaries 3 Quantitative Specification on Top of Maude 4 Probabilistic Model Checking 5 Statistical Model Checking 6 Implementation 7 Case Studies 7.1 The Probabilistic Language Prob 7.2 Head-of-Line Blocking and HTTP/3 8 Evaluation 9 Related Work 10 Conclusions References Concurrency and Memory Models Minimisation of Spatial Models Using Branching Bisimilarity 1 Introduction 2 Preliminaries 3 CoPa-Bisimilarity for QdCM 4 From QdCMs to Labelled Transition Systems 4.1 General Encoding for Finite CMs 4.2 Optimised Encoding for Symmetric Finite CMs 5 Feasibility Study 5.1 Implementation 5.2 Experimental Setup 5.3 Results and Discussion 6 Conclusions and Future Work References Reasoning About Promises in Weak Memory Models with Event Structures 1 Introduction 2 Motivating Examples 3 A Weak Memory Semantics with Promises 4 Event Structures 5 Reasoning 5.1 Semantics of Assertions 5.2 Proof Rules 5.3 Soundness and Completeness 6 Related Work 7 Conclusion References A Fine-Grained Semantics for Arrays and Pointers Under Weak Memory Models 1 Introduction 2 A Versatile Language with Fine-Grained Concurrency 3 Non-atomic Language 3.1 Structured Arrays 3.2 Pointers 3.3 Unstructured Arrays (Arrays of Pointers) 4 Instruction-Level Parallelism 4.1 Reordering and Refinement 4.2 Array Indexing and Reordering 5 Applications 5.1 Aliasing and Reordering 5.2 Linked Lists and the Treiber Stack 5.3 The Meltdown Vulnerability 6 Related Work 7 Conclusion References VeyMont: Parallelising Verified Programs Instead of Verifying Parallel Programs 1 Introduction 2 Overview of VeyMont – The ``Inverted Workflow'' 3 Overview of VeyMont – More Features 4 Design and Implementation 4.1 Parser (Step 1a) 4.2 Linter (Step 1a) 4.3 Annotator (Step 1b) 4.4 VerCors (Step 1c) 4.5 Code Generator (Step 2) 5 Evaluation 6 Future Work A Appendix: Parallelisation of Tic-Tac-Toe References Verification 2 Verifying Functional Correctness Properties at the Level of Java Bytecode 1 Introduction 2 Motivating Examples 3 How ByteBack Works 3.1 Specifying Functional Properties 3.2 Translating Grimp into Boogie 3.3 Implementation Details 4 Experiments 4.1 Programs 4.2 Results 5 Related Work 6 Conclusions References Abstract Alloy Instances 1 Introduction 2 Example 3 Preliminaries 3.1 Alloy Semantics 3.2 Alloy Analyses 4 Abstract Alloy Instances 4.1 Properties of Abstract Instances 5 Computing Abstract Alloy Instances 5.1 Encoding of Bounds in Alloy 5.2 Running Time Complexity 5.3 Different Upper Bound Kinds 5.4 Implementation and Visualization 6 Evaluation 6.1 RQ1: Overhead 6.2 RQ2: Size Comparison 6.3 RQ3: Diversity 6.4 RQ4: Impact of Upper Bound Kind 6.5 Threats to Validity 7 Related Work 8 Conclusion References Monitoring the Internet Computer 1 Introduction 2 Background 3 Policies 3.1 Methodology 3.2 Policy Formulas 4 Evaluation 5 Lessons Learned 6 Related Work 7 Conclusion References Word Equations in Synergy with Regular Constraints 1 Introduction 2 Overview 3 Preliminaries 4 Stability of String Constraints 4.1 Stability of Single-Equation Systems 4.2 Stability of Multi-equation Systems 4.3 Constructing Inclusion Graphs and Chain-Freeness 5 Algorithm for Satisfiability Checking 5.1 Refining Language Assignments by Noodlification 5.2 Satisfiability Checking by Refinement Propagation 5.3 Working with Shortest Words 6 Experimental Evaluation 7 Related Work 8 Conclusion and Future Work References Formal Methods in AI Verifying Feedforward Neural Networks for Classification in Isabelle/HOL 1 Introduction 2 Isabelle and Higher-Order Logic (HOL) 2.1 Isabelle/HOL 2.2 Isabelle as Formal Methods Framework 3 Running Example: Classifying Lines in a Grid 4 Modelling Neural Networks in Isabelle 4.1 Data Modelling 4.2 Encoding Our Running Example 4.3 Evaluating Neural Networks 4.4 Compliance of Our Formalisation to TensorFlow 5 Properties of Classification Networks 6 Implementation 7 Classifying Digits of a 5 7 Matrix Display 8 Related Work 9 Conclusion and Future Work References SMPT: A Testbed for Reachability Methods in Generalized Petri Nets 1 Introduction 2 Technical Background 3 Design and Implementation 4 Commands, Basic Usage and Installation 5 Comparison with Other Tools 6 Future Work References The Octatope Abstract Domain for Verification of Neural Networks 1 Introduction 2 Preliminaries 2.1 Linear, UTVPI, and Difference Constraints 2.2 Minimum Cost Network Flow Problem 2.3 Verification of Neural Networks 3 Abstract Domains: Octatopes and Hexatopes 3.1 Zonotopes and Linear Star Sets 3.2 Octatopes and Hexatopes 3.3 Linear Optimization Over Octatopes and Hexatopes 3.4 Intersection of Octatopes/Hexatopes and Half-Spaces 4 Range Computation for Neural Nets with Prefilters 5 Experimental Results 6 Conclusion References Program Semantics and Verification Technique for AI-Centred Programs 1 Introduction and Preliminaries 1.1 Preliminaries and Background 1.2 Our Contributions 2 Logical Languages LFO and LmDK 2.1 Syntax of LFO , LmK, and LmDK 2.2 Semantics of LFO and LmDK 3 Programming Language PL 3.1 Syntax of PL 3.2 Relational Semantics of PL 3.3 Weakest Precondition Semantics of PL 3.4 Equivalence Between the Two Program Semantics 4 Translating LmDK to LFO 5 Implementation 5.1 Mechanisation of Our LmDK-to-FO Translation 5.2 Case Study 1: Dining Cryptographers' Protocol ch27Chaum1988 5.3 Case Study 2: Cheryl's Birthday Puzzle ch27van2017cheryl 6 Related Work 7 Conclusions References Safety and Reliability Tableaux for Realizability of Safety Specifications 1 Introduction 2 Preliminaries. Safety Specifications and Games 3 Realizability Tableaux 3.1 Terse Normal Form 3.2 Tableaux 3.3 Subsumption and Syntactical Inconsistency 3.4 Tableau Rules 3.5 A Tableau Algorithm for Realizability 4 Conclusions References A Decision Diagram Operation for Reachability 1 Introduction 2 Preliminaries 2.1 Binary Decision Diagrams 2.2 Multi-valued Decision Diagrams 2.3 Decision Diagram Operations 2.4 Encoding Symbolic Transition Systems 2.5 Reachability with Decision Diagrams 2.6 Saturation 3 Decision Diagram Operation for Reachability 3.1 For BDDs 3.2 Analysis 3.3 MDD Generalization 3.4 Correctness 4 Empirical Evaluation 4.1 Experimental Setup 4.2 Results 5 Conclusion References Formal Modelling of Safety Architecture for Responsibility-Aware Autonomous Vehicle via Event-B Refinement 1 Introduction 2 Preliminaries 2.1 Safety Architecture 2.2 Responsibility-Sensitive Safety (RSS) 2.3 Modelling and Proving in Event-B 3 Example: Goal-Aware RSS for Pull over Scenario 4 Case Study 1: Modelling Subscenario S4 4.1 Machine M4,0: Whole Controller-Level Behaviour 4.2 Machine M4,1: Module-Level Behaviour 4.3 Machine M4,2: Manoeuvre-Level Behaviour 5 Case Study 2: Modelling Subscenario S3 5.1 Machine M3,0: Whole Controller-Level Behaviour 5.2 Machine M3,1: Module-Level Behaviour 5.3 Machine M3,2: Manoeuvre-Level Behaviour 6 Discussion 6.1 Model Engineering 6.2 Generality of Approach 6.3 Using Event-B for Modelling and Proving 6.4 Related Work 7 Conclusion References A Runtime Environment for Contract Automata 1 Introduction 2 Modal Service Contract Automata 3 CARE Design 4 Formal Guarantees 5 Building Applications with CARE 6 Examples and Evaluation 7 Conclusion References Industry Day Formal and Executable Semantics of the Ethereum Virtual Machine in Dafny 1 Introduction 2 Background and Motivation 3 The Dafny-EVM 4 Practical Experiences 5 Related Work 6 Conclusion References Shifting Left for Early Detection of Machine-Learning Bugs 1 Introduction 2 Background 3 Static Analysis Framework 3.1 Code Representation 3.2 Query Language 4 Analysis Rules 4.1 Issues Specific to Computational Notebooks 4.2 Misuses of Deep Learning Libraries 5 Experimental Evaluation 6 Related Work 7 Conclusion References A Systematic Approach to Automotive Security 1 Introduction 2 Trusted Methodology 3 Automotive Security by Design 3.1 System Architecture Model 3.2 Threat Analysis 3.3 V&V Planning 4 Automotive Security Testing 4.1 Automata Learning for Correctness 4.2 Use-Case Scenarios 5 Conclusion References Specification-Guided Critical Scenario Identification for Automated Driving 1 Introduction 2 Specification-Driven Scenario-Based Testing 2.1 Traffic Scenario Description 2.2 Critical Scenario Identification 2.3 Formal Specifications 2.4 Sampling Strategy 3 Automatic Emergency Braking Case Study 3.1 Simulation Results 3.2 Lessons Learned References Runtime Monitoring for Out-of-Distribution Detection in Object Detection Neural Networks 1 Introduction 2 Preliminaries 2.1 Neural Networks 2.2 Gaussian-Based White-Box Monitoring 2.3 Inductive Conformal Anomaly Detection 3 Monitoring Algorithm 3.1 Extension to Object Detection Neural Networks 3.2 Embedding into the Framework of Inductive Conformal Anomaly Detection 4 Experiments 5 Conclusion and Future Work References Backdoor Mitigation in Deep Neural Networks via Strategic Retraining 1 Introduction 2 Preliminaries 2.1 Deep Neural Networks 2.2 Artificial Brain Stimulation Analysis 3 Methodology 4 Experiments 4.1 Experiment Setup 4.2 Mitigation Results 5 Conclusion References veriFIRE: Verifying an Industrial, Learning-Based Wildfire Detection System 1 Introduction 2 The VeriFIRE Project 3 Conclusion and Remaining Challenges A Background: DNNs and Their Verification References Author Index This book constitutes the refereed proceedings of the 25th International Symposium on Formal Methods, FM 2023, which took place in Lubeck, Germany, in March 2023. The 26 full paper, 2 short papers included in this book were carefully reviewed and selected rom 95 submissions.