Software Engineering and Formal Methods: 21st International Conference, SEFM 2023, Eindhoven, The Netherlands, November 6-10, 2023, Proceedings (Lecture Notes in Computer Science)

This book constitutes the refereed proceedings of the 21st International Conference on Software Engineering and Formal Methods, SEFM 2023, held in Eindhoven, The Netherlands, during November 6-10, 2023. The 18 regular papers presented in this book, together with 1 invited paper and 1 tool paper, were carefully reviewed and selected from 41 submissions. The SEFM conference series aims to bring together researchers and practitioners from academia, industry and government, to advance the state of the art in formal methods, to facilitate their uptake in the software industry, and to encourage their integration within practical software engineering methods and tools. Preface Organization Randomized Testing of Distributed Systems (Abstract) Contents Invited Contribution Herding CATs 1 Introduction 2 CATs by Example 2.1 General Structure of a CAT 2.2 Accessing the Program State: Observation Quantifiers 2.3 Running Example 2.4 Goal of Specification 2.5 CATs 3 Wrapping Up References Regular Papers Refinements for Open Automata 1 Introduction 2 Open Automata and Their Composition 2.1 Preliminaries and Notations 2.2 Open Automata (OA) 2.3 Relations Between Open Automata 2.4 A Bisimulation for Open Automata 2.5 Reachability 3 Simulation for Automata with the Same Holes 4 A Simulation Relation that Takes Holes into Account 5 Properties of Our Simulation Relations 5.1 Non-blocking Composition 5.2 Properties 6 Related Work 7 Conclusion References The Cubicle Fuzzy Loop: A Fuzzing-Based Extension for the Cubicle Model Checker 1 Introduction 2 Backgound on Cubicle 3 Motivation 4 Fuzzing Cubicle 5 Experimental Results and Discussion 6 Conclusion and Related Work References Guiding Symbolic Execution with A-Star 1 Introduction 2 Running Example 3 A* Guided Symbolic Execution 4 Guiding the Exploration Towards the Unknown 5 Application to Binary Programs 6 Experimental Results 7 Conclusion References Robustness Testing of Software Verifiers 1 Introduction 2 Background 3 Robustness Testing for Software Verification 3.1 Robustness of Software Verifiers 3.2 Semantics-Preservation 3.3 Transformations 3.4 Robustness Testing Through Repeated Transformations 4 Evaluation 4.1 Benchmark Setup 4.2 Experimental Results 5 Related Work 6 Conclusion References Decoupled Fitness Criteria for Reactive Systems 1 Introduction 2 Preliminaries 3 A Formal Framework for Capturing Fitness 4 Reducing Fitness Evaluation to Matrix Analysis 4.1 Step [stepspsrecur]2: Constructing the Recurrence Relation 4.2 Step [stepspsmatrix]3: Matrix Analysis 5 Case Studies 5.1 Case Study #1: Simple Communication Protocol 5.2 Case Study #2: Two Phase Commit (2PC) 5.3 Case Study #3: Alternating Bit Protocol (ABP) 6 Related Work 7 Conclusions and Future Work References Capturing Smart Contract Design with DCR Graphs 1 Introduction 2 Background 2.1 Smart Contracts: Ethereum and Solidity 2.2 Dynamic Condition Response Graphs 3 Smart Contract Design Patterns as DCR Graphs 4 Modeling and Analysis of a Casino Smart Contract 5 Related Work 6 Conclusion and Future Work References An Active Learning Approach to Synthesizing Program Contracts 1 Introduction 2 Motivating Example 3 Background 3.1 Contracts 3.2 Register Automata 3.3 Active Learning of Register Automata 4 Contract Synthesis 4.1 Learning a Behavioural Model 4.2 Generating Contracts from a Register Automaton 4.3 Correctness and Optimality 5 Implementation 6 Evaluation 7 Related Work 8 Conclusion References Ranged Program Analysis via Instrumentation 1 Introduction 2 Background 2.1 Program Syntax and Semantics 2.2 Program Ranges 2.3 Ranged Program Analysis 3 Ranged Program Analysis via Instrumentation 3.1 Instrumenting Programs with Ranges 3.2 From Test Cases to Branching Decisions 3.3 Instrumentation-Based Ranged Analysis 3.4 Handling Underspecified Bounds 4 Implementation 5 Evaluation 5.1 Evaluation Setup 5.2 RQ1: Comparison of the CPA-Based and Instrumentation-Based Ranged Program Analysis 5.3 RQ2: Comparing Range Instrumentation and Range Reduction 5.4 RQ3: Comparison of Instrumentation-Based Ranged Analysis with Standalone Execution 5.5 Threats to Validity 6 Related Work 7 Conclusion References Attack Time Analysis in Dynamic Attack Trees via Integer Linear Programming 1 Introduction 2 Related Work 3 Dynamic Attack Trees 3.1 Semantics 3.2 The Min Time Metric 3.3 Relation to Semantics of ch10Budde2021 4 An MILP Approach to Min Time 5 Computation Time Reduction 5.1 Bottom-Up Computation 5.2 Modular Analysis 6 Experiments 6.1 Generation of Testing DATs 6.2 Time Comparisons 7 Conclusion and Discussion References SSCalc: A Calculus for Solidity Smart Contracts 1 Introduction 2 Background 2.1 Inductive Data Types 2.2 State Monad 2.3 State 2.4 Exceptions 3 Calculus 3.1 Basic Rules 3.2 Method Invocation 4 Formalization in Isabelle/HOL 4.1 Verification of Soundness 4.2 Automation 5 Methodology 6 Case Study: Verified Banking 6.1 The Contract 6.2 Formalizing the Contract 6.3 Specification of Properties 6.4 Verification 7 Related Work 8 Conclusion References ATM: A Logic for Quantitative Security Properties on Attack Trees 1 Introduction 1.1 Our Approach 1.2 Related Work 2 Attack Trees 2.1 Security Metrics for Attack Trees 3 A Logic for at General Metrics 3.1 Syntax of ATM 3.2 Semantics of ATM 4 Case Study: Attacking a CubeSAT 5 Model Checking Algoritms 5.1 Binary Decision Diagrams (BDDs) 5.2 BDDs from ATs and Layer 1 Formulae 5.3 Model Checking Layer 1 Formulae 5.4 Model Checking Layer 2 Formulae 5.5 Compute Metrics for Layer 3 Formulae 5.6 Model Checking Layer 4 Formulae 6 Conclusions References Refactoring of Multi-instance BPMN Processes with Time and Resources 1 Introduction 2 Models 3 Refactoring 4 Tool and Experiments 5 Related Work 6 Concluding Remarks References Verified Scalable Parallel Computing with Why3 1 Introduction 2 An Overview of Why3 2.1 Specifying and Verifying Functional Programs with Why3 2.2 Limitations with Higher-Order Functions 3 Functional Bulk Synchronous Parallelism 4 Formalization of BSML Core and Standard Library 5 Verified Scalable Maximum Prefix Sum 6 Related Work 7 Conclusion and Future Work References Exact and Efficient Bayesian Inference for Privacy Risk Quantification 1 Introduction 2 Background 2.1 Privug: A Data Privacy Debugging Method 2.2 Multivariate Gaussian Distributions 3 Exact Inference Engine for Privug 3.1 Semantics 3.2 Soundness and Termination 4 Case Study: Privacy Risks in Public Statistics 5 Scalability Evaluation 6 Related Work 7 Conclusion References A Formalization of Heisenbugs and Their Causes 1 Introduction 2 A Formalization of Heisenbugs 2.1 System Model 2.2 Formal Definition of Heisenbugs 3 Causality 3.1 Modeling Sources of Nondeterminism 3.2 Defining Causes 3.3 Causes and Nondeterminism 3.4 Testing and Causal Analysis 4 Analysis Methodology and Challenges 5 Related Work 6 Conclusion References Verifying Read-Copy Update Under RC11 1 Introduction 2 Motivation 2.1 ABA Problem During Memory Reclamation 2.2 An RCU-Based Solution 2.3 Execution Under RC11 Memory 3 Background 3.1 Syntax and RC11 Semantics 3.2 Owicki-Gries Reasoning 3.3 View-Based Assertions 4 Extensions to Semantics and Logic 4.1 Allocation Model 4.2 Extending the Assertion Language 5 Proof of Correctness 5.1 Ownership and Capabilities 5.2 Invariants and Proof Outlines 6 Related and Future Work 7 Conclusions References QNNRepair: Quantized Neural Network Repair 1 Introduction 2 Related Work 2.1 Neural Network Verification 2.2 Neural Network Repair 2.3 Quantized Aware Training 3 Preliminaries 3.1 Statistical Fault Localization 3.2 Neural Network and Quantization 3.3 Solvers for Mixed Integer Linear Optimization 4 QNNRepair Methodology 4.1 Ranking the Importance of the Neurons 4.2 Constraints-Solving Based Repairing 4.3 QNNRepair Algorithm 5 Experiment 5.1 Experimental Setup 5.2 Repair Results on Baselines 5.3 Comparison with Data-Free Quantization 5.4 Repair Efficiency 5.5 Comparison Between Fault Localization Metrics in QNNRepair 5.6 Limitations 6 Conclusion References Timeout Prediction for Software Analyses 1 Introduction 2 Background 2.1 Programs and Control Flow Automata 2.2 Predicate Analysis 2.3 CEGAR 3 Features for Learning 4 Timeout Prediction 5 Evaluation 5.1 Evaluation Setup 5.2 Metrics 5.3 RQ1: Comparing Static Features to Dynamic Ones, Which Feature Set Leads to a Better Performing Model? 5.4 RQ2: Can a Machine Learning Model Outperform Simple Heuristics? 5.5 RQ3: Does a Sequential Composition Benefit from a Timeout Prediction? 6 Related Work 7 Conclusion References Tool Papers PMC-VIS: An Interactive Visualization Tool for Probabilistic Model Checking 1 Introduction 2 Background and Related Work 3 PMC-VIS: Visualising Probabilistic Model Checking 4 Usage Scenarios and Performance 5 Conclusion References Author Index