Formal Methods : 26th International Symposium, FM 2024, Milan, Italy, September 9–13, 2024, Proceedings, Part I

Preface Organization Contents – Part I Contents – Part II Invited Papers Adversarial Robustness Certification for Bayesian Neural Networks 1 Introduction 2 Background on Bayesian Deep Learning 3 Problem Statement 3.1 Decision Robustness 3.2 Approach Outline 4 BNN Adversarial Robustness via Weight Sets 4.1 Bounding Probabilistic Robustness 4.2 Bounding Decision Robustness 4.3 Computation of the Lower and Upper Bounds 5 Explicit Bound Computation 5.1 Integral Computation over Weight Intervals 5.2 Bounding Bayesian Neural Network Output 6 Complete Bounding Algorithm 6.1 Lower-Bounding Algorithm 6.2 Upper-Bounding Algorithm 7 Experiments 7.1 Airborne Collision Avoidance 7.2 Image Classification 8 Conclusion References Getting Chip Card Payments Right 1 Introduction 1.1 Attacks on EMV 1.2 Applying Formal Methods 1.3 Contributions 2 Background 2.1 The C8 Protocol 2.2 The Tamarin Prover 3 Tamarin Model of C8 3.1 Protocol Model 3.2 Security Properties 3.3 Analysis Approach 4 Results 4.1 Secure Configurations 4.2 Insecure Configurations 4.3 Privacy 4.4 Relay Resistance 5 Conclusion A Lemmas B Acronyms References Fundamentals of Formal Verification A Local Search Algorithm for MaxSMT(LIA) 1 Introduction 2 Preliminary 2.1 MaxSMT on Linear Integer Arithmetics 2.2 Local Search Components 3 Review of LS-LIA 4 Pairwise Operator 4.1 Motivation 5 Compensation-Based Picking Heuristic 5.1 Pairwise Operation Candidates for Compensation 5.2 Two-Level Heuristic 5.3 Algorithm for Picking a Pairwise Operation 6 Local Search Algorithm 7 Experiments 7.1 Experiment Preliminaries 7.2 Comparison to Other MaxSMT Solvers 7.3 Evolution of Solution Quality 7.4 Effectiveness of Proposed Strategies 8 Discussion on the Extension of Pairwise Operation 9 Conclusion and Future Work References Integrating Loop Acceleration Into Bounded Model Checking 1 Introduction 2 Preliminaries 3 From BMC to ABMC 3.1 Bounded Model Checking 3.2 Accelerated Bounded Model Checking 3.3 Fine Tuning Acceleration 4 Guiding ABMC with Blocking Clauses 5 Related Work 6 Experiments and Conclusion References Nonlinear Craig Interpolant Generation Over Unbounded Domains by Separating Semialgebraic Sets 1 Introduction 2 Preliminaries 2.1 Quadratic Module 2.2 Homogenization 2.3 Problem Description 3 Existence of Interpolant 3.1 Interpolant Between (x) and (x) 3.2 Interpolant Between (x,y) and (x,z) 4 Sum-of-Squares Formulation 4.1 SOS Characterization for Polynomial Interpolants 4.2 SOS Characterization for Semialgebraic Interpolants 5 Synthesizing Interpolant via SOS Programming 6 Conclusions and Future Work References Practical Approximate Quantifier Elimination for Non-linear Real Arithmetic 1 Introduction 2 Algorithm 2.1 Problem Definition 2.2 Our Overapproximation Algorithm 2.3 Our Implication Oracle 2.4 Removing the Satisfiability Oracle 3 Experimental Results 4 Conclusion References A Divide-and-Conquer Approach to Variable Elimination in Linear Real Arithmetic 1 Introduction 2 Preliminaries 3 A Divide-and-Conquer Approach 3.1 Divide: The FMplex Method 3.2 Conquer: Obtaining a Conjunctive Result 3.3 Further Improvements 4 Relation to Virtual Term Substitution 5 Experimental Evaluation 6 Conclusion References Foundations Free Facts: An Alternative to Inefficient Axioms in Dafny 1 Introduction 2 Dafny and Its Verifier 2.1 Proof Obligations 2.2 Axioms Versus Assumptions 2.3 Expression Translation 3 Free Facts 3.1 Motivating Example 3.2 Free Facts 3.3 Free Facts for Collection Types 3.4 Discussion 4 Evaluation 4.1 Research Questions 4.2 Methodology 4.3 Results and Discussion 4.4 Threats to Validity 5 Related Work 6 Conclusion References Understanding Synthesized Reactive Systems Through Invariants 1 Introduction 1.1 Related Work 2 Preliminaries 3 Computing Mixed Monotone/Antitone Invariants 3.1 Computing a Set of Mixed Monotone/antitone Invariants 4 Experiments and Case Studies 4.1 GUI Glue Code Synthesis 4.2 Generalized Buffer 5 Conclusion References Combining Classical and Probabilistic Independence Reasoning to Verify the Security of Oblivious Algorithms 1 Introduction 2 Overview 2.1 Challenges for Verification 2.2 Mixing Probabilistic and Classical Reasoning 3 Preliminaries 3.1 Programming Language and Semantics 4 Logic 4.1 Assertions 4.2 Judgements and Rules 4.3 Soundness 4.4 Oversights in Original PSL 5 Case Studies 6 Related Work 7 Conclusion and Future Work References Efficient Formally Verified Maximal End Component Decomposition for MDPs 1 Introduction 2 Background 3 Correctness of the MEC Algorithm 3.1 Abstract MDP Structure 3.2 Specification 3.3 Abstract Algorithm 4 Data Structures and Refinement 4.1 Supplementary Data Structures 4.2 The mcsta Data Structure 4.3 Filter List 5 Code Generation and Integration 5.1 Compatibility with mcsta 6 Experimental Evaluation 6.1 Experimental Setup 6.2 Results 7 Conclusion References Introducing SWIRL: An Intermediate Representation Language for Scientific Workflows 1 Introduction 2 Background and Related Work 2.1 Related Work 2.2 Scientific Workflow Models 2.3 Distributed Workflow Models 3 The SWIRL Representation 3.1 Semantics 3.2 Workflow Model Encoding 3.3 Consistency of SWIRL Semantics 4 Optimisation 5 Implementation 6 Evaluation 7 Conclusion References Fast Attack Graph Defense Localization via Bisimulation 1 Introduction 2 Illustrative Example 3 Preliminaries 3.1 Monotonic Criteria and Cores 3.2 Bisimulation Relations 3.3 Analytical Attack Graphs 4 The Defense Problem and a Naive Defense Algorithm 5 Applying Bisimulation to Attack Graphs, and a Fast Defense Algorithm 5.1 Folding an AAG 5.2 The AF-Defense Algorithm 6 Evaluation 7 Related Work 8 Conclusion and Future Work References Learn and Repair State Matching and Multiple References in Adaptive Active Automata Learning 1 Introduction 2 Overview 3 Preliminaries 4 L# with Rebuilding 4.1 Observation Trees 4.2 The L# Algorithm 4.3 Rebuilding in L# 5 L# Using State Matching 5.1 State Matching 5.2 Optimised Separation Using State Matching 5.3 Approximate State Matching 6 Adaptive L# 7 Adaptive Learning with Multiple References 8 Experimental Evaluation 9 Conclusion References Automated Repair of Information Flow Security in Android Implicit Inter-App Communication 1 Introduction 2 Preliminaries 2.1 Android Basics 2.2 How Intent Communication Works 2.3 An Example of the Challenges of Implicit Intent Communication 3 Methodology 3.1 An Abstract Model of Implicit Intents 3.2 How Intent Repair Works 3.3 Implementation 4 Evaluation 4.1 RQ1: Effectiveness of [0.5]IntentRepair 4.2 RQ2: Scalability of [0.5]IntentRepair 4.3 Discussion 5 Related Work 6 Conclusions and Future Work References Learning Branching-Time Properties in CTL and ATL via Constraint Solving 1 Introduction 2 Preliminaries 2.1 Concurrent Game Structure (CGS) and Kripke Structure 2.2 Alternating-Time Temporal Logic 3 Passive Learning for ATL 3.1 SAT-Based Learning Algorithm 3.2 Deciding the Separability 4 Experimental Evaluation 5 Conclusion References A Zonotopic Dempster-Shafer Approach to the Quantitative Verification of Neural Networks 1 Introduction 2 Problem Statement 3 Analysis with Interval Dempster-Shafer Structures 4 Analysis with Probabilistic Zonotopes 5 Analysis with Zonotopic Dempster-Shafer Structures 6 Evaluation 7 Conclusion References Certified Quantization Strategy Synthesis for Neural Networks 1 Introduction 2 Preliminaries 3 Our Approach 3.1 Foundation of Quadapter 3.2 Overview of Quadapter 3.3 Template T2i of Preimage P2i 3.4 Details of Function UnderPreImage 3.5 Checking (A"0362A2i)P2i 4 Applications: Robustness and Backdoor-Freeness 4.1 Certified Quantization for Robustness 4.2 Certified Quantization for Backdoor-Freeness 5 Evaluation 5.1 Performance of UnderPreImage Function 5.2 Certified Quantization for Robustness 5.3 Certified Quantization for Backdoor-Freeness 6 Related Work 7 Conclusion References Partially Observable Stochastic Games with Neural Perception Mechanisms 1 Introduction 2 Background 3 One-Sided Neuro-Symbolic POSGs 4 Values of One-Sided NS-POSGs 5 P-PWLC Value Iteration 6 Heuristic Search Value Iteration for NS-POSGs 6.1 Lower and Upper Bound Representations 6.2 One-Sided NS-HSVI 6.3 Belief Representation and Computations 7 Experimental Evaluation 8 Conclusions References Bridging Dimensions: Confident Reachability for High-Dimensional Controllers 1 Introduction 2 Background and Problem Setting 3 Verification of High-Dimensional Systems 4 Experimental Evaluation 5 Related Work 6 Conclusion References VeriQR: A Robustness Verification Tool for Quantum Machine Learning Models 1 Introduction 2 Robustness for Quantum Machine Learning Models 2.1 Quantum Machine Learning Model 2.2 Robustness Verification of QML Models 2.3 Challenges of Implementation 3 Overview and Features of VeriQR 3.1 Verifying Robustness 3.2 Improving Robustness 4 Evaluation 4.1 Local Robustness 4.2 Global Robustness 5 Conclusion References Programming Languages Formal Semantics and Analysis of Multitask PLC ST Programs with Preemption 1 Introduction 2 Preliminaries 3 Multitask PLC and a Running Example 4 Formal Semantics of Multitask PLC 4.1 K Configuration for Multitask PLC 4.2 K Rules for Multitask PLC 4.3 Example of K Rule Applications 5 Time Abstraction 5.1 Abstraction Function 5.2 Equivalence Before and After Abstraction 6 State Space Reduction 6.1 Our Ample Set Approach 6.2 Internal Transitions Without Memory Update 7 Experimental Evaluation 8 Related Work 9 Concluding Remarks References Accurate Static Data Race Detection for C 1 Introduction 2 Multi-threaded C Programs 3 Encoding Data Race Checking as Reachability 4 Experimental Evaluation 5 Related Work 6 Conclusion References cfaults: Model-Based Diagnosis for Fault Localization in C with Multiple Test Cases 1 Introduction 2 Preliminaries 3 Model-Based Diagnosis with Multiple Test Cases 4 cfaults: MBD with Multiple Observations for C 5 Experimental Results 6 Related Work 7 Conclusion References Detecting Speculative Execution Vulnerabilities on Weak Memory Models 1 Introduction 2 Speculative Execution Attacks 2.1 Spectre-PHT 2.2 Spectre-PHT and Weak Memory 3 Background 3.1 Weakest Precondition Based Information Flow Reasoning 3.2 Extending with Rely/Guarantee Reasoning 3.3 Reordering Interference Freedom 4 Information Flow Logic 4.1 Weakest Precondition with Speculation 4.2 Rely/Guarantee and Reordering 4.3 Reordering Interference Freedom 4.4 Example Revisited 4.5 Discussion 5 Related Work 6 Conclusion References Staged Specification Logic for Verifying Higher-Order Imperative Programs 1 Introduction 2 Illustrative Examples 2.1 A Simple Example 2.2 Pre/Post Vs Staged Specifications via foldr 2.3 Inferrable Vs User-Provided Specifications via map 3 Language and Specification Logic 3.1 Semantics of Staged Formulae 3.2 Compaction 4 Forward Rules for Staged Logics 5 Staged Entailment Checking and Its Soundness 6 Implementation and Initial Results 7 Related Work 8 Conclusion References Unifying Weak Memory Verification Using Potentials 1 Introduction 2 Motivation 3 Background 4 A Logic for Potentials 5 Example Proofs 6 Lifting SC and TSO to Potentials 7 Soundness of Rules in Memory Models 8 Conclusion References Proving Functional Program Equivalence via Directed Lemma Synthesis 1 Introduction 2 Motivation and Approach Overview 3 Preliminary 4 AutoProof in Detail 4.1 The Overall Approach 4.2 Induction-Friendly Forms in AutoProof 4.3 General Routine of Tactics 4.4 Tactic 1: Removing Compositions 4.5 Tactic 2: Switching Recursive Arguments 4.6 Properties 5 Evaluation 6 Related Work 7 Conclusion References Reachability Analysis for Multiloop Programs Using Transition Power Abstraction 1 Introduction 2 Preliminaries 3 Multi-loop Analysis with TPA 3.1 Overview 3.2 Core Algorithm 3.3 Running Example 3.4 Correctness 3.5 Witness Production 4 Evaluation 5 Related Work 6 Conclusion References Logic and Automata Misconceptions in Finite-Trace and Infinite-Trace Linear Temporal Logic 1 Introduction 2 Background 2.1 ltlf Example: Concision via Finiteness 2.2 Toward a Concept Inventory 3 Instrument Design 3.1 ltlf Instrument 3.2 ltl Instruments 4 Data 4.1 Student : 2023 and 2024 4.2 FTAI: 2023 4.3 Student : 2022 5 Catalog Design 6 Results: Incorrect Responses, Specific Errors 7 Results: Categories of Errors 7.1 Length (ltlf only) 7.2 Last (ltlf only) 7.3 Cycle G 7.4 Implicit Prefix 7.5 Trace-Split U 7.6 Spreading X 8 Threats to Validity 9 Related Work 10 Looking Forward References Sound and Complete Witnesses for Template-Based Verification of LTL Properties on Polynomial Programs 1 Introduction 2 Transition Systems, LTL and Büchi Automata 3 Sound and Complete B-PA Witnesses 3.1 Sound and Complete Witnesses for Existential B-PA 3.2 Sound and Complete Witnesses for Universal B-PA 4 Template-Based Synthesis of Polynomial Witnesses 5 Experimental Results 6 Conclusion References The Opacity of Timed Automata 1 Introduction 2 Preliminaries 2.1 Timed Words, Timed Languages and Timed Automata 2.2 Expressiveness and Decidability of Timed Automata 3 Opacity Problems of Timed Automata 3.1 Language-Based and Location-Based Timed Opacity 3.2 Transformation Between LBTO, ILTO and CLTO 4 Decidability and Undecidability of Timed Opacity Problems 4.1 Undecidability of Opacity Problems of OTA 4.2 Decidability in the Discrete-Time Semantics 4.3 Sufficient Condition and Necessary Condition 5 Discussion and Conclusion References Parameterized Verification of Round-Based Distributed Algorithms via Extended Threshold Automata 1 Introduction 2 System Model 2.1 Abstract Threshold Automata 3 Specifications 4 CS vs ACS 5 Checking General Parameterized Coverability 5.1 Well-Structured Transition Systems 5.2 Abstract Counter Systems as WSTS 5.3 WSTS-Based General Parameterized Coverability Checking 5.4 Correctness 6 Reachability via (0,1)-Abstraction 6.1 Parameterized Reachability Algorithm (PRA) 7 Implementation and Experimental Evaluation 8 Related Work 9 Conclusion References The Nonexistence of Unicorns and Many-Sorted Löwenheim–Skolem Theorems 1 Introduction 2 Preliminaries 2.1 Many-Sorted First-Order Logic 2.2 Model-Theoretic Properties 2.3 Notation 3 The Nonexistence of Unicorns 3.1 Motivating the Proof 3.2 Ramsey's Theorem and Generalizations 3.3 The Proof of Theorem 3 3.4 Applications to Theory Combination 4 Many-Sorted Löwenheim–Skolem Theorems 4.1 Lost in Translation 4.2 Downward, Upward, and Combined Versions 4.3 A Stronger Result for Split Signatures 4.4 An Application: The Łoś–Vaught Test 5 Conclusion References Author Index