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