Fundamental Approaches to Software Engineering: 23rd International Conference, FASE 2020, Held as Part of the European Joint Conferences on Theory and ... Computer Science and General Issues)

ETAPS Foreword
Preface
Organization
Contents
Invited Talk
Improving symbolic automata learning  with concolic execution
	1 Introduction
	2 Preliminaries
		2.1 Symbolic finite state automata
		2.2 Active learning and minimally adequate teachers
		2.3 Concolic execution
		2.4 From path conditions to SFA
	3 Active learning for SFA
		3.1 Learning using observation tables
		3.2 Learning using discrimination trees
	4 Active learning with concolic execution
		4.1 Concolic learning with symbolic observation tables
		4.2 Concolic learning with a symbolic membership oracle
	5 Experimental evaluation
		5.1 Experimental Setup
		5.2 Learning with symbolic observation tables
		5.3 Learning with symbolic membership queries
	6 Related work
		6.1 Active learning
		6.2 Passive learning
	7 Conclusions
	References
FASE Contributions
Platinum: Reusing Constraint Solutions in Bounded Analysis of Relational Logic
	1 Introduction
	2 Illustrative Example
	3 Approach
		3.1 Slicing
		3.2 Canonicalization
		3.3 Storing and Reuse
	4 Empirical Study
		4.1 Objects of Analysis
		4.2 Variables and Measures
		4.3 Study Operation
		4.4 Threats to Validity
		4.5 Results for RQ1 (Small Changes)
		4.6 Results for RQ2 (Successive Changes)
		4.7 Results for RQ3 (Scope Changes)
		4.8 Results for RQ4 (Overhead)
		4.9 Results for RQ5 (Real-World Specifications)
	5 Related Work
	6 Conclusions
	Acknowledgment
	References
Integrating Topological Proofs with ModelChecking to Instrument Iterative Design
	1 Introduction
	2 TOrPEDO
	3 Background
	4 Revising models
	5 TOrPEDO automated support
	6 Evaluation
	7 Related work
	8 Conclusions
	Acknowledgments
	References
A Generalized Formal Semantic Framework forSmart Contracts
	1 Introduction
	2 Preliminaries
		2.1 Smart Contracts
		2.2 The K-framework
	3 A General Semantic Model
		3.1 Syntax
		3.2 Configuration
		3.3 Semantics of the Core Features
	4 Direct Semantics Generation
	5 Evaluation
	6 Conclusion
	Acknowledgements
	References
An Empirical Study on the Use and Misuseof Java 8 Streams
	1 Introduction
	2 Motivating Example and Conceptual Background
	3 Study Subjects
	4 Stream Characteristics
		4.1 Methodology
		4.2 Results
		4.3 Discussion
	5 Stream Usage
		5.1 Methodology
		5.2 Results
		5.3 Discussion
	6 Stream Misuses
		6.1 Methodology
		6.2 Results
	7 Threats to Validity
	8 Related Work
	9 Conclusion & Future Work
	Acknowledgments
	References
Extracting Semantics from Question-Answering Services for Snippet Reuse
	1 Introduction
	2 Related Work
	3 StackSearch: A Semantic-aware Snippet Recommender
		3.1 Overview
		3.2 Preprocessor
		3.3 Word Model Builder
		3.4 Metadata Extractor
		3.5 Querying Engine
	4 Evaluation
		4.1 Evaluation using Programming Queries
		4.2 Evaluation using Post Links
		4.3 Comparative Evaluation
	5 Conclusion
	Acknowledgements
	References
Global Reproducibility through Local Control for Distributed Active Objects
	1 Introduction
	2 Motivating Example
	3 A Formal Model of Reproducibility
		3.1 A Basic Active Object Language
		3.2 An Operational Semantics for the Basic Language
		3.3 A Labelled Operational Semantics for the Basic Language
		3.4 Execution Traces and their Reordering
	4 Global Reproducibility with Local Traces
	5 Extensions for Richer Active Object Languages
	6 Implementing Record & Replay for Real-Time ABS
		6.1 Recording Traces in a Distributed Setting
		6.2 Names in the Erlang Simulator
		6.3 Visualization of Recorded Traces
		6.4 Example
		6.5 Performance Characteristics of the Implementation
	7 Related Work
	8 Conclusion and Future Work
	References
Multi-level Model Product Lines Open and closed variability for modelling language families
	1 Introduction
	2 Multi-level modelling: intuition and challenges
		2.1 Multi-level modelling, by example
		2.2 Improving reuse in multi-level modelling: some challenges
	3 A formal foundation for multi-level modelling
	4 Multi-level model product lines
	5 Tool support
	6 Related work
	7 Conclusions and future work
	Acknowledgments
	Appendix
	References
Computing Program Reliability using Forward-Backward Precondition Analysis and Model Counting
	1 Introduction
	2 Motivating Examples
	3 Forward-Backward Precondition Analyses
	4 Computing Success and Failure Probabilities
	5 Extension to non-deterministic programs
	6 Implementation
	7 Related work
	8 Conclusion
	References
Skill-Based Verification of Cyber-Physical Systems
	1 Introduction
	2 Background on Hybrid-System Modeling
	3 A Formalization for Skill-Based Modeling
		3.1 Formalizing Skills
		3.2 Formalizing Skill Graphs
		3.3 Composition of Skill Graphs
	4 Compositional Verification of Skill Graphs
		4.1 Verification Condition Generation
		4.2 Assembling Hybrid Programs in a Skill graph
		4.3 Integration into the Software Development Process
	5 Evaluation and Discussion
		5.1 Open-Source Implementation
		5.2 Case Study: Vehicle Follow Mode
		5.3 Results
	6 Related Work
	7 Conclusion and Future Work
	Acknowledgements
	References
Generating Large EMF Models Efficiently A Rule-Based, Configurable Approach*
	1 Introduction
	2 Related Work
		2.1 Solver-Based Approaches
		2.2 A Tableaux-Based Approach
		2.3 Rule-Based Approaches
		2.4 A Hybrid Approach
		2.5 Need for Further Research
	3 Running Example and Preliminaries
		3.1 Running Example
		3.2 The Eclipse Modeling Framework
		3.3 Transformation Rules and Transformation Units
		3.4 EMF Repair
	4 Rule-Based Instance Generation
		4.1 Overall Approach
		4.2 Generated Rules for Model Generation
		4.3 Generation Strategies: Parameterization
		4.4 User Interaction
		4.5 Limitations and Formal Guarantees
	5 Tooling
	6 Evaluation
		6.1 Scalability Experiments
		6.2 Diversity Experiment
		6.3 Threats to Validity
	7 Conclusion and Future Work
	References
Family-Based SPL Model Checking Using Parity Games with Variability
	1 Introduction
	2 Preliminaries
	3 Software Product Lines Model Checking
	4 Variability Parity Games and SPL Model Checking
		4.1 Variability Parity Games
		4.2 Solving SPL Model Checking Using Variability Parity Games
	5 Recursively Solving Variability Parity Games
	6 Implementation and Experiments
		6.1 Minepump Case Study
		6.2 Elevator Case Study
	7 Conclusions
	References
Model-based tool support for Service Design
	1 Motivation
	2 Technological Solution
		2.1 Conceptual Architecture
		2.2 Development Process
	3 Related Works
	Acknowledgements
	References
Incremental Concurrent Model Synchronization using Triple Graph Grammars
	1 Introduction
	2 Preliminaries
		2.1 Triple Graph Grammars
		2.2 Model Update and Model Synchronization
		2.3 Dependency Relations
	3 Synchronizing Solutions for Concurrent Updates
	4 An Incremental Procedure CSynch
		4.1 Marking
		4.2 Repairing and Conflict-Solving
		4.3 Properties of CSynch
	5 Related Work
	6 Conclusion
	References
Statistical Model Checking forVariability-Intensive Systems
	1 Introduction
	2 Background on Model Checking
		2.1 Linear Temporal Logic
		2.2 Statistical Model Checking
		2.3 Model Checking for VIS
		2.4 Other Related Work
	3 Family-Based Statistical Model Checking
		3.1 Random Sampling in Featured BŁuchi Automata
		3.2 Hypothesis Testing
		3.3 Lower Bound (Minimum Number of Samples)
		3.4 Upper Bound (Maximum Number of Samples)
	4 Empirical Study
		4.1 Objectives and Methodology
		4.2 Experimental Setup
	5 Results
		5.1 RQ1: Detection Rate
		5.2 RQ2: Eficiency
		5.3 RQ3: Family-based SMC versus Enumerative SMC
	6 Conclusion
	References
Schema Compliant Consistency Management via Triple Graph Grammars and Integer Linear Programming
	1 Introduction
	2 Running Example
	3 Main Ideas
	4 Related Work
	5 Preliminary Definitions
	6 Correctness and Completeness
	7 Implementation and Experimental Evaluation
	8 Extension to Other Operations
	9 Conclusion and Future Work
	Acknowledgements
	References
Towards Multiple Model Synchronization with Comprehensive Systems
	1 Introduction
	2 Preliminaries: Multimodelling
	3 Use Case
	4 State of the Art
	5 Comprehensive Systems
		5.1 Typed Local Models
		5.2 Extending the Base Language
		5.3 Metamodel and Model Commonalities
		5.4 Reusing Methods of Local Model Management
		5.5 Advantages over Model Merge
	6 Categorical Formalization
		6.1 Theoretical Background and Notation
		6.2 Comprehensive System
		6.3 Multimodel Equivalence
	7 Conclusion, Related Work and Future Plans
	References
Analysis and Refactoring of Software Systems Using Performance Antipattern Profiles
	1 Introduction
	2 Running Example
		2.1 System description
		2.2 External services
		2.3 Internal components
		2.4 Operational profile parameters
	3 Approach
		3.1 Overview
		3.2 Detection rules
		3.3 Synthesis of antipattern profiles
		3.4 Refactoring
	4 Evaluation
		4.1 Research questions
		4.2 Experimental scenarios
		4.3 Experimental Results
		4.4 Threats to validity
	5 Related Work
	6 Conclusion
	References
Business Process Compliance using Reference Models of Law
	1 Introduction
	2 Regulatory Compliance Framework
	3 DCR Graphs
		3.1 Semantics
	4 Compliance Rules
	5 Compliance Checking by Refinement
	6 Adoption considerations
	7 Related Work
	8 Concluding Remarks
	References
Algorithmic Analysis of Blockchain Efficiency with Communication Delay
	1 Introduction
	2 An Overview of Proof-of-work Blockchains
	3 A Random Network Model for Blockchains
	4 Algorithmic Analysis of Blockchain Efficiency
		4.1 Network Simulation with a Priority Queue
		4.2 A Faster Simulation Algorithm
		4.3 An Approximation Algorithm for Unbounded Number of Workers
	5 Empirical Evaluation of Blockchain Efficiency
	6 Related Work and Concluding Remarks
	References
Holistic Specifications for Robust Programs
	1 Introduction
	2 Motivating Example: The Bank
	3 Chainmail Overview
	4 Overview of the Formal foundations
		4.1 Chainmail judgments
		4.2 An underlying programming language, Loo
	5 Assertions
		5.1 Satisfaction of Assertions - Access, Control, Space, Viewpoint
		5.2 Satisfaction of Assertions - Time
		5.3 Properties of Assertions
		5.4 Modules satisfying assertions
	6 Examplar Driven Design
	7 Related Work
	8 Conclusions
	9 Acknowledgments
	References
Automated Generation of Consistent Graph Models with First-Order Logic Theorem Provers
	1 Introduction
	2 Preliminaries
		2.1 Models and metamodels
		2.2 Model predicates and Well-formedness constraints
		2.3 First-Order Logic Theorem Provers
	3 Overview of the Approach
	4 From Domain-Specific Languages to First-Order Logic
		4.1 Mapping Types in the Metamodel
		4.2 Mapping Relations Between Metamodel Types
		4.3 Instance model mapping
		4.4 Mapping additional constraints
	5 Evaluation
		5.1 Research Question 1 (RQ1)
		5.2 Research Question 2 (RQ2)
		5.3 Threats to validity
	6 Related work
	7 Conclusion and Future Work
	References
Combining Partial Specifications using Alternating Interface Automata
	1 Introduction
		1.1 Conjunction for Inputs and Outputs
		1.2 Conjunctions of states
		1.3 Contributions
	2 Preliminaries
	3 Alternating Interface Automata
		3.1 Alternation
		3.2 Input-Failure Semantics for AIAs
		3.3 AIA Determinization
		3.4 Connections between IAs and AIAs
	4 Testing Input-Failure Refinement
		4.1 Testers for AIA Specifications
		4.2 Test Cases for AIA Specifications
	5 Conclusion and Future Work
	Acknowledgement
	References
Revisiting Semantics of Interactions for Trace Validity Analysis
	1 Introduction
	2 Interaction language and denotational semantics
		2.1 Base syntax
		2.2 Denotational semantics for basic interactions
		2.3 Extension of the language with loops
	3 Operational Semantics
		3.1 Frontier actions
		3.2 Pruning
		3.3 Execute function and operational semantics
	4 Back-to-back comparison of both semantics
	5 Trace analysis
	6 Related work
	7 Conclusion
	References
Test-Comp Contributions
Second Competition on Software Testing: Test-Comp 2020
	1 Introduction
	2 Definitions, Formats, and Rules
	3 Categories and Scoring Schema
	4 Reproducibility
	5 Results and Discussion
	6 Conclusion
	References
HybridTiger: Hybrid Model Checking and Domination-based Partitioning for Efficient Multi-Goal Test-Suite Generation (Competition Contribution)
	1 Software Architecture
	2 Test-Generation Approach
	3 Strengths and Weaknesses
	4 Setup and Configuration
	5 Project and Contributors
	References
ESBMC: Scalable and Precise Test Generation based on the Floating-Point Theory (Competition Contribution)
	1 Test Generation Approach
	2 Strengths and Weaknesses
	3 Tool Setup and Configuration
	4 Software Project
	References
TracerX: Dynamic Symbolic Execution with Interpolation (Competition Contribution)
	1 Overview and Software Architecture
	2 Discussion on Strengths and Weaknesses
	3 Tool Setup and Configuration
	4 Software Project and Contributors
	References
LLVM-based Hybrid Fuzzing with LibKluzzer (Competition Contribution)
	1 Test Generation Approach
	2 Software Architecture
	3 Strengths and Weaknesses
	4 Tool Setup and Configuration
	5 Software Project and Contributors
	References
CoVeriTest with Dynamic Partitioning of the Iteration Time Limit (Competition Contribution)
	1 Test-Generation Approach
	2 Tool Architecture
	3 Strengths and Weaknesses
	4 Setup and Configuration
	5 Project and Contributors
	References
LEGION: Best-First Concolic Testing (Competition Contribution)
	1 Test-Generation Approach
	2 Tool Description & Configuration
	3 Discussion
	References
Author Index