Theoretical Aspects of Software Engineering: 16th International Symposium, TASE 2022, Cluj-Napoca, Romania, July 8–10, 2022, Proceedings (Lecture Notes in Computer Science Book 13299)

This book constitutes the proceedings of the 16th International Conference on Theoretical Aspects of Software Engineering, TASE 2022, held in Cluj-Napoca, Romania, July 2022. The 21 full regular papers presented together with 5 short papers in this book were carefully reviewed and selected from 71 submissions. The topics of the papers covering various fields in software engineering and the latest developments in in formal and theoretical software engineering methods and techniques. Preface Organization Keynotes Neural Network Discrimination: Evaluation, Mitigation and Certification SMT Solving: Historical Roots, Recent Developments and Future Directions Rigorous System Design for AI Software Contents Practical Theory of Computation on Structures 1 Introduction 2 Towards a Theory of Computation on Structures 3 Insignificant Non-determinism 3.1 Abstract State Machines 3.2 Polynomial-Time-Bounded ASMs 3.3 Insignificant Choice ASMs 3.4 PTIME Logics 3.5 Recursive Syntax 3.6 PTIME Verification References Complexity of Distributed Petri Net Synthesis 1 Introduction 2 Preliminaries 3 Distributability 4 Complexity Analysis 5 Conclusion References Repairing Adversarial Texts Through Perturbation 1 Introduction 2 Background 3 Our Repair Approach 3.1 Adversarial Text Detection 3.2 Semantic-Preserving Perturbation 3.3 Voting for the Correct Label 3.4 Overall Algorithm 4 Experiments 4.1 Experimental Settings 4.2 Research Questions 4.3 Threats to Validity 5 Related Work 6 Conclusion References Formal Verification of a Keystore 1 Introduction 1.1 Related Work 1.2 The Keystore 1.3 Verification Objectives 2 Methodology 2.1 The Code 2.2 Abstract Specification 2.3 C Code 2.4 Refinement 2.5 Simulation 2.6 Integration 3 Standard Library Connection 3.1 Heap Abstraction 3.2 The Connector 4 Discussion 4.1 Verification 4.2 Lessons Learned 4.3 Future Research 4.4 Conclusion References A Case Study in the Automated Translation of BSV Hardware to PVS Formal Logic with Subsequent Verification 1 Introduction 2 Preliminaries 3 Computational Model 4 Optimizations Addressing Scalability 5 Case Study: RapidIO Encoder 6 Related Work 7 Conclusion References Sound Static Analysis of Regular Expressions for Vulnerabilities to Denial of Service Attacks 1 Introduction 2 Background 2.1 ReDoS Vulnerabilities 2.2 ReDoS Detection 2.3 Regexes Basics 2.4 Regex Matching 3 Semantics 4 Detection of ReDoS Vulnerabilities 5 Experimental Evaluation 6 Related Work 7 Conclusions References On Verification of Smart Contracts via Model Checking 1 Introduction 2 Related Work 3 Solidity and VERDS 3.1 Solidity 3.2 Model Checking Tool VERDS 4 Overview of mcVer Framework 5 Smart Contract Modeling 6 Scenario Configuration and Specification Formulation 6.1 Scenario Configuration 6.2 Specification 7 Verification and Counter Example Extraction 8 Case Studies and Experiments 8.1 Security Vulnerabilities Checking 8.2 Access Control Contract 9 Conclusion and Future Work References Equivalence of Denotational and Operational Semantics for Interaction Languages 1 Introduction 2 Basic Interactions and Intuition of Their Meaning 2.1 Preliminaries 2.2 Basic Interactions 2.3 Repetition Operators on Sets of Traces 3 Syntax and Denotational Semantics 4 A Structural Operational Semantics 4.1 Termination 4.2 Dealing with Weak-Sequencing Using Evasion and Pruning 4.3 Execution Relation and Operational Semantics 4.4 Illustrative Example 5 Proving the Equivalence of both Semantics 6 Related Works 7 Conclusion and Further Work References Automatic Classification of Bug Reports Based on Multiple Text Information and Reports’ Intention 1 Introduction 2 Related Work 3 Methodology 3.1 Preprocessing 3.2 Feature Extraction 3.3 Classifier 4 Experiment 4.1 Dataset 4.2 Evaluation Metrics 4.3 Results 5 Discussion 5.1 Experiment Analysis 5.2 Threats to Validity 6 Conclusion and Future Work References Collaborative Verification of Uninterpreted Programs 1 Introduction 2 Motivation 3 Collaborative Verification Framework 4 Preliminary Result 5 Related Work 6 Next Steps 7 Conclusion References MSDetector: A Static PHP Webshell Detection System Based on Deep-Learning 1 Introduction 2 Motivation 2.1 Framework Overview 2.2 Motivating Example 3 MSDetector 3.1 Pre-training Transformer Model 3.2 Training Transformer Model and Detecting Webshell 4 Experiment and Evaluation 4.1 Experimental Configuration and Evaluation Criteria 4.2 Datasets 4.3 Experiments for Answering RQ1 4.4 Experiments for Answering RQ2 4.5 Experiments for Answering RQ3 5 Limitations 6 Related Work 6.1 Static Webshell Detection 6.2 Code Representation 6.3 Pre-trained Models for Programming Languages 7 Conclusions References Extending Process Algebra with an Undefined Action 1 Motivation and Related Work 2 Labelled Transition Systems: Basics 3 Basic Extended Process Algebra (BXPA) 4 Lifted Strong Bisimulations and PHML 5 Conclusion References Machine-Assisted Proofs for Institutions in Coq 1 Introduction 2 Mathematical Background 2.1 First-Order Predicate Logic 3 Institutions in Coq 4 First-Order Logic in Coq 4.1 Representing FOL 4.2 Proofs and Proof Strategy 5 Formalizing EVT 5.1 Representing EVT 5.2 Proofs and Proof Strategy 6 Conclusion References Optimizing Trans-Compilers in Runtime Verification Makes Sense – Sometimes 1 Introduction 2 TeSSLa and Its Reference Compiler 3 The TeSSLa Compiler and Optimizations 3.1 Expansion of the Language Core and the DSL 3.2 Usage of Smart Initializations Within the Monitors 4 Evaluation 5 Summary References Testing Vehicle-Mounted Systems: A Stepwise Symbolic Execution Approach for OSEK/VDX Programs 1 Introduction 2 OSEK/VDX Background and Motivating Example 2.1 Scheduler of OSEK/VDX OS 2.2 Running Example 3 Symbolic Execution for OSEK/VDX Programs 3.1 Overview 3.2 Sequentialization of OSEK/VDX Programs 3.3 Background of Symbolic Execution Techniques 3.4 Stepwise Symbolic Execution 4 Experiment and Evaluation 4.1 Experiments and Benchmarks 4.2 Experimental Results 5 Related Work 6 Conclusion and Future Work References Dynamic Specification Mining Based on Transformer 1 Introduction 2 Preliminary 2.1 Seq2seq Model 2.2 Attention Mechanism 2.3 Transformer Model 3 Dynamic Specification Mining Based on Transformer 3.1 Trace Generating 3.2 Transformer Model Learning 3.3 Trace Sampling 3.4 Feature Extraction 3.5 Cluster Analysis 3.6 Model Selection 4 Experiment 4.1 DataSet 4.2 Experience Setting 4.3 Experiment Results and Analyses 5 Related Work 5.1 Mining Properties Expressed in Temporal Logic Formulas 5.2 Mining Properties Expressed in FSA-Like Model 6 Conclusion References Dynamic Environment Simulation for Database Performance Evaluation 1 Introduction 2 Related Work 3 Workload Generator Definition 3.1 Workload Generator Definition 4 Environment Simulation 4.1 Workload Modeling on Each Individual Dimension 4.2 Modeling Environment by Learning Workload Interaction Among Dimensions 4.3 Dynamic Environment Simulation 5 Experiment Results 5.1 Environment Workload Demonstration 5.2 Environment Simulation 5.3 Evaluation on Database 6 Conclusion References Extending SysML with Refinement and Decomposition Mechanisms to Generate Event-B Specifications 1 Introduction 2 Background 2.1 SysML 2.2 Event-B 3 SysML Extensions with Refinement and Decomposition Mechanisms 3.1 SysML Package Diagram Extensions 3.2 SysML Sequence Diagram Extension 4 Illustration of the SysML Extensions 5 SysML to Event-B Translation 5.1 Translation Rules 5.2 Implementation 5.3 Discussion 6 Related Work 7 Conclusion References Development of Monitoring Systems for Anomaly Detection Using ASTD Specifications 1 Introduction 2 Related Work 3 Case Study 3.1 Graphical Specification of the IDS 3.2 Action Definitions 3.3 IDS Code Generation 3.4 Example of Specification Execution 4 Evaluation and Discussion 5 Conclusion References A Language-Based Causal Model for Safety 1 Introduction 2 Preliminaries 3 A Railway Crossing Example 4 A Language-Based Causal Model 5 Computing Causes 6 Experimental Evaluation 7 Extensions 8 Conclusions References Consistency of Heterogeneously Typed Behavioural Models: A Coalgebraic Approach 1 Introduction and Motivation 2 Running Example 3 Background 3.1 Notation 3.2 Coalgebras 3.3 Signature Morphisms 3.4 Predicate Lifting 3.5 Temporal Operators 4 Formula Translation 4.1 Truth Preservation 4.2 The Case Study Revisited 4.3 Handshaking 5 Related Work 6 Future Work References Improving Adversarial Robustness of Deep Neural Networks via Linear Programming 1 Introduction 2 Preliminaries 2.1 Deep Neural Networks 2.2 Adversarial Robustness 3 Training for Adversarial Robustness 3.1 Generating Easily-Misclassified Examples 3.2 Improving Adversarial Robustness with Easily-Misclassified Examples 4 Experiments 4.1 Effect of Parameters 4.2 Performance on Adversarial Examples Generation 4.3 Performance on Robust Training 5 Related Work 6 Conclusion References AllSynth: Transiently Correct Network Update Synthesis Accounting for Operator Preferences 1 Introduction 2 A Model for Update Synthesis 2.1 Routing Policies 2.2 Update Synthesis 2.3 Simple Update Sequence Reordering 3 The AllSynth Tool and the Synthesis Algorithm 4 Implementation and Evaluation 5 Conclusion References End-to-End Heat-Pump Control Using Continuous Time Stochastic Modelling and Uppaal Stratego 1 Introduction 2 Usecase and Method 2.1 Methodological Overview 3 Thermal Model Identification 4 Modelling in Uppaal Stratego 4.1 Learning by Stratego 4.2 Online Synthesis 5 Evaluation 6 Conclusion References Security Vulnerabilities Detection Through Assertion-Based Approach 1 Introduction 2 Assertion Construction 3 Conclusion References The Complexity of Evaluating Nfer 1 Introduction 2 The Inclusive Nfer Language 3 Complexity Results for Inclusive Nfer 4 The Full Nfer Language 5 Minimality 6 Discussion and Conclusion References Supporting Algorithm Analysis with Symbolic Execution in Alk 1 Introduction 2 Alk - An Educational Algorithmic Language/Framework 2.1 Syntax 2.2 Semantics 2.3 Concrete and Symbolic Executions 3 Understanding Algorithms by Experimentation 4 Understanding Loops 5 Understanding the Use of Algorithms 6 Hints for Estimating Execution Time 7 Conclusion References Author Index