Theoretical Aspects of Software Engineering: 16th International Symposium, TASE 2022, Cluj-Napoca, Romania, July 8–10, 2022, Proceedings

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