Theoretical Aspects of Software Engineering : 18th International Symposium, TASE 2024, Guiyang, China, July 29 – August 1, 2024, Proceedings

This book constitutes the refereed proceedings of the 18th International Symposium on Theoretical Aspects of Software Engineering, TASE 2024, held in Guiyang, China, during July 29–August 1, 2024. The 24 full papers, 2 short papers, 1 invited abstract and 1 invited papers were carefully selected from 76 submissions. The papers presented new results on innovative advances in software engineering, as well as the latest developments in formal and theoretical software engineering methods and techniques. Preface Organization DSL Engineering via Lifting Transformation (Invited Abstract) Contents Protocol Conformance of Collaborative SPARQL Using Multiparty Session Types 1 Introduction 2 Preliminaries and Examples 2.1 RDF and SPARQL 2.2 Multiparty Session Types 3 Overview 4 Implementation of SQT Workflow 5 Evaluation 6 Conclusion References Composition Machines: Programming Self-organising Software Models for the Emergence of Sequential Program Spaces 1 Introduction 2 Related Work 3 Preliminaries 3.1 Category Theory 3.2 Quiver Foundations 4 Semantics of Composition and Program Spaces 5 Composition Machines 6 Example 7 Conclusions References Slicing Assisted Program Verification: An Empirical Study 1 Introduction 2 Preliminaries 2.1 Program Slicing 2.2 Program/System Dependence Graph 3 Related Work 4 Experimental Evaluation 4.1 Research Questions 4.2 Experimental Setup 5 Experimental Results 5.1 RQ1: Result Consistency 5.2 RQ2: Efficiency Improvement 5.3 RQ3: Program Types 6 Discussion 6.1 Programs Features 6.2 Various Verification Technique 6.3 Limitations of Tools/Toolchains 7 Conclusions and Future Work References An Approach to Improving Reliability of Parallel Graph Computation 1 Introduction 2 Preliminaries 2.1 Pregel Computation 2.2 MSVL Language 2.3 Runtime Verification at Code Level 3 An Approach for Verifying Pregel Computation 3.1 Modeling the Parallel Graph Computation 3.2 Converting a Property into a MSVL Program 3.3 Runtime Verification with MSVL 4 Case Studies 4.1 Case Study A: The Shortest Paths Problem 4.2 Case Study B: PageRank Algorithm 5 Conclusion References Safe and Infinite Resource Scheduling Using Energy Timed Automata 1 Introduction 2 Energy Timed Automata 2.1 Constrained Safety 2.2 Flat and Segmented ETAs 3 Infinite Runs in Flat SETAs 3.1 Binary Resource Relations 3.2 Resource Functions 3.3 Post Fixed Points of Resource Functions 3.4 Putting It All Together 4 Non-linear Limit Sets 4.1 Expressiveness of ETPs 4.2 R* with Multiple Resources 5 Conclusion References Intrathread Method Orders Based Adaptive Testing of Concurrent Objects 1 Introduction 2 Intrathread Method Order 3 Our Approach IMOACT 3.1 Intrathread Method Orders Based Adaptive Test Generation 3.2 Key Scheduling Point Based Scheduling 4 Experiments 4.1 RQ1 - Efficiency with Key Scheduling Points Based Schedules 4.2 RQ2 - Concurrency Bug Detection Capabilities 4.3 RQ3 - Maximum Step Size 5 Related Work 6 Conclusion References An Abstract Interpretation-Based Data Leakage Static Analysis 1 Introduction 2 Background 2.1 Data Frame-Manipulating Programs 2.2 Trace Semantics 3 Concrete Data Leakage Semantics 3.1 (Absence of) Data Leakage 3.2 Dependency Semantics 3.3 Data Leakage Semantics 4 Data Leakage Analysis 4.1 Data Sources Abstract Domain 4.2 Abstract Data Leakage Semantics 5 Experimental Evaluation 6 Related Work 7 Conclusion References On the Decidability of Disassembling Binaries 1 Introduction 2 Related Work 3 Overview 3.1 Theorems 3.2 Meta Theorem 4 Formalization 5 Discussion 5.1 Self-modification 5.2 The Oracles 6 Conclusion References Finding Deep-Hidden Bugs in Android Apps via Functional Semantics Guided Exploration 1 Introduction 2 Background 2.1 DMFs in Apps 2.2 Q-Learning for Android Testing 3 Empirical Study 3.1 App Collection 3.2 Identify GUI Patterns of DMFs 3.3 Rule Definition for Extracting DMFs 4 Approach 4.1 DMF Extraction While Depth-First Exploration 4.2 Functional Semantics Guided Q-Leaning Exploration 5 Evaluation 5.1 Experiment Setup 5.2 Experimental Results 6 Related Work 7 Conclusion References Detecting Vulnerabilities via Explicitly Leveraging Vulnerability Features on Program Slices 1 Introduction 2 Background and Related Work 2.1 Program Slicing Technique 2.2 Related Work 3 Approach 3.1 GRU Statement Embedding 3.2 Constructing VulDict 3.3 Model Training 3.4 Model Inference 4 Experimental Design 4.1 Research Questions 4.2 Experimental Dataset 5 Experimental Results 6 Conclusion References Fuzzing for Stateful Protocol Implementations: Are We There Yet? 1 Introduction 2 Background 2.1 Terminologies of Stateful Protocol 2.2 General Workflow of Stateful Protocol Fuzzers 3 Study Design 4 Evaluation Results and Findings 4.1 RQ1. Effectiveness of Code Coverage 4.2 RQ2. Effectiveness of State Machine Coverage 4.3 RQ3. Bug Revealing Capability 4.4 RQ4. Evaluation on Test Throughput 4.5 Summary and Analyze 5 Threats to Validity 6 Related Work 7 Conclusion References CtxFuzz: Discovering Heap-Based Memory Vulnerabilities Through Context Heap Operation Sequence Guided Fuzzing 1 Introduction 2 Motivation 3 Methodology 3.1 Overview of CtxFuzz 3.2 Context Heap Operation Sequence Feedback 3.3 Instrumentation 3.4 Fuzzing Loop and Seed Selection 4 Evaluation 4.1 Experiment Setup 4.2 RQ1. Vulnerability Detection Capability 4.3 RQ2. Compare with Other SOTA Fuzzers 4.4 RQ3. Ablation Studies 4.5 Discussion 5 Related Work 6 Conclusion References An Adaptive Real-Time Garbage Collection Method Based on File Write Prediction 1 Introduction 2 Background and Motivation 2.1 Flash Devices and Flash File Systems 2.2 Garbage Collection 2.3 Real-Time Requirement and Task Periodicity in Embedded Systems 3 Real-Time Garbage Collection 3.1 Design Overview 3.2 Periodic Write Behavior Prediction 3.3 Adaptive Trigger Garbage Collection 3.4 Multi-condition Victim Block Selection Algorithm 3.5 Partition Record of Victim Blocks 3.6 Correctness of Prediction Algorithm 4 Evaluation 4.1 Experimental Setup 4.2 Experimental Results 4.3 Real-World Applications Experimental Results 5 Conclusion and Future Work References Tree-Based Synthesis of Web Test Sequences from Manual Actions 1 Introduction 2 Background and Challenges 3 The Fret Test Generation Framework 3.1 Overview 3.2 The Action Mutator 3.3 The Action Sequencer 4 Evaluation 4.1 Research Questions 4.2 Subject Websites 4.3 Experimental Setup 4.4 RQ1: Similar Element Detection 4.5 RQ2: Mutation Sequence Legality 4.6 RQ3: Mutation Sequence Redundancy 4.7 RQ4: Tool Usefulness 5 Threats to Validity 6 Related Work 7 Conclusions and Future Work References Gradual Typing Performance, Micro Configurations and Macro Perspectives 1 Introduction 2 Background 3 Benchmarks and Evaluation Protocol 4 Representativeness of Outlying Configurations 5 Time Variations of Intermediate Configurations 6 Related Work 7 Conclusion References ISS-Scenario: Scenario-Based Testing in CARLA 1 Introduction 2 Related Works 3 ISS-Scenario Scenario Library 4 Batch Scenario Testing 5 Case Studies 6 Conclusion References Verified Validation for Affine Scheduling in Polyhedral Compilation 1 Introduction 2 Background 2.1 Overview of Polyhedral Models 2.2 Validation via Bernstein's Conditions 3 Language Setting 3.1 Polyhedral Models 3.2 Instruction Language Interface 4 Validation Algorithm and Its Proofs 4.1 Validation Algorithm 4.2 Proof Goal and Its Sketch 5 Evaluation 5.1 Support Existing Verified Compiler 5.2 Support Existing Polyhedral Compiler 5.3 Engineering Efforts 6 Related Work 6.1 Verification of Polyhedral Compilation 6.2 Verification of Tensor Compilation 6.3 Verified Validation for Compiler Optimization 7 Conclusions and Future Work References A Formally Verified Scheme for Security Protocols with the Operational Semantics of Strand Space 1 Introduction 2 Related Work 3 Preliminaries 3.1 Formal Strand Specification 3.2 Strand Space 3.3 Murphi 4 Operational Semantics of Strand Space 5 The Verification Framework 6 Verification Towards 5G EAP-TLS Protocol 7 Conclusion and Future Work References Empirically Scalable Invariant Generation Leveraging Divide-and-Conquer with Pruning 1 Introduction 2 Preliminaries 3 An Overview of Our Approach 3.1 The Original Approaches ch19DBLP:confspscavspsColonSS03,ch19DBLP:confspssasspsSankaranarayananSM04,ch19DBLP:journalsspspacmplspsLiuFYSL22 3.2 Divide-and-Conquer Strategy 3.3 Pruning Strategy 4 Divide-and-Conquer Strategy 5 Pruning Strategy 5.1 Path-Recording Multi-step-Backtracking Pruning (PMP) 5.2 Full-Scope-Predictive Forward-Checking Pruning (FFP) 6 Evaluation 7 Related Work 8 Conclusion References DeepCDCL: A CDCL-based Neural Network Verification Framework 1 Introduction 2 Background 2.1 Neural Network Verification Problem 2.2 Traditional Verification Techniques 3 DeepCDCL Verification Framework 3.1 Overview of DeepCDCL 3.2 Solver Module 3.3 Clause Manager Module 3.4 Implementation and Optimization 4 Evaluation 5 Related Work 6 Conclusion References Energy-Efficient Motion Planning for Autonomous Vehicles Using Uppaal Stratego 1 Introduction 2 Related Work 3 Preliminaries 3.1 Reinforcement Learning 3.2 Uppaal Stratego 4 Use Case and Models 4.1 Vehicle's Kinematic Model 4.2 Energy Model 4.3 Abstract View of Vehicle Model 5 Vehicle Model in Uppaal Stratego 5.1 Strategy Synthesis 6 Assertion-Based Concatenated Motion Planning 7 Experimental Evaluation 7.1 RQ1: Impact Factors on the Synthesis Methods' Performance 7.2 RQ2: Performance Improvement of Learning with CoMOP 7.3 RQ3: Time-Efficient and Energy-Efficient Motion Plans 8 Conclusions and Future Work References CFStra: Enhancing Configurable Program Analysis Through LLM-Driven Strategy Selection Based on Code Features 1 Introduction 2 Background and Motivation 3 Methodology 3.1 Code Snippet Extraction 3.2 Code Feature Identification 3.3 Strategy Selection 4 Evaluation 4.1 Experimental Setup 4.2 Performance of Different Strategies 4.3 Compared to Other SOTA Combination Strategies 4.4 Ablation Study 4.5 Threats to Validity 5 Related Work 6 Conclusions References Improved Incremental Verification for Neural Networks 1 Introduction 1.1 Neural Network Verification 1.2 Incremental Verification for Neural Network 1.3 Contributions of This Paper 2 Preliminaries 2.1 Neural Networks 2.2 Branch-and-Bound for Verification 2.3 Incremental Verification 3 Improved Incremental Verification 3.1 Overview of I-IVAN 3.2 Append 3.3 Record and Combine 3.4 Algorithm for I-IVAN 4 Experiments 4.1 Experiment Configurations 4.2 Comparison on Quantized Networks 4.3 Contribution of Append and Combine 4.4 The Generalization of I-IVAN 5 Related Work 6 Conclusion References Automatic Construction of HD Maps for Simulation-Based Testing of Autonomous Driving Systems 1 Introduction 2 Related Work 3 Preliminaries 3.1 OpenDRIVE Framework 3.2 Map Model 4 Automatic Generation of HD Maps 4.1 Junction Topology 4.2 Generation of Junction Layouts 4.3 Instantiation 5 Evaluation 5.1 Implementation 5.2 Setup 5.3 Experimental Results 6 Conclusion References Managing Traceability for Software Life Cycle Processes 1 Introduction 2 Traceability 3 Management of Traceable Systems 3.1 Adding a Model Element 3.2 Inactivating a Model Element 3.3 Modifying a Model Element 3.4 Modifying a Dependency Relation 3.5 Relocating a Model Element 3.6 Replacing a Model Element 3.7 Merging Two Model Elements 3.8 Decomposing a Model Element 3.9 Maintenance of Traceability 3.10 Restriction of Structure Models 4 Tool 5 Related Work 6 Conclusion and Future Work References A Natural Formalized Proof Language 1 Introduction 2 Proof Language Design 3 The Formal Semantics of Proof Language 4 The Workflow of ProofGrader 4.1 Overall Architecture 4.2 Proof Parsing 4.3 Static Analysis 4.4 Proof Checking 5 Solver Manager 6 Evaluation 6.1 Performance 6.2 Comparison of Features 7 Related Work 8 Conclusion References Strong Forgetting in Hennessy-Milner Logic 1 Introduction 2 Preliminaries 2.1 Calculus of Communicating Systems 2.2 Hennessy-Milner Logic 3 Strong Forgetting on Actions 3.1 Strong Bisimulation Discarding Actions 3.2 Strong Forgetting on Actions 3.3 Sufficient and Necessary Conditions 4 Concluding Remarks References Author Index