Intro
Preface
Organization
Abstracts of Invited Talks
Compositional Reasoning at The Software/Hardware Interface
Separation of Concerns for Complexity Mitigation in System and Domain Formal Modelling - A Dive into Algebraic Event-B Theories
A Foundation for Interaction
Practical Verified Concurrent Program Security
On Analysing Weak Memory Concurrency
Certified Proof and Non-Provability
Verifying Compiler Optimisations
Contents
Invited Paper
Verifying Compiler Optimisations
1 Introduction
2 Data-Flow Sub-graphs
3 Term Rewriting Rules

4 Verifying Term Rewriting Rules
5 Generating Code for Optimisations
6 Conclusions
References
Regular Papers
An Idealist's Approach for Smart Contract Correctness
1 Introduction
2 Overview
2.1 Smart Contracts
2.2 Vulnerability and Correctness
2.3 An Illustrative Example
3 Specification Language
3.1 High-Level Overview
3.2 Formalization
4 Verification
4.1 Function Validation
4.2 Generating Proof Obligations
5 Implementation and Evaluation
5.1 Implementation
5.2 Experimental Evaluation
6 Related Work and Conclusion
References

Active Inference of EFSMs Without Reset
1 Introduction
2 Background and Related Work
2.1 Running Example
2.2 Related Work
2.3 Definitions
2.4 Inferring Functions with Genetic Programming
3 The ehW-Inference Algorithm
3.1 Assumptions
3.2 Homing and Characterizing
3.3 Inputs and Data Structures
3.4 ehW-Inference Backbone
3.5 Generalisation
3.6 Oracle Procedure
4 Inferring a Vending Machine Controller
5 Conclusions and Future Work
References
Learning Mealy Machines with Local Timers
1 Introduction
2 Related Work
3 Preliminaries

3.1 Mealy Machines
3.2 The Rivest-Schapire Algorithm
4 Mealy Machines with Local Timers
4.1 Syntax and Semantics
4.2 Expanded Forms and Equivalence
5 Learning MMLTs Efficiently
5.1 Timer Queries
5.2 Timed Counterexample Analysis
5.3 Hypothesis Refinement
5.4 Hypothesis Completion
5.5 Output Query Complexity
6 Practical Evaluation
7 Conclusion and Future Work
References
Compositional Vulnerability Detection with Insecurity Separation Logic
1 Introduction
2 Motivation
3 Attacker Model
4 Insecurity Separation Logic (InsecSL)

5 Symbolic Execution
6 Implementation
7 Evaluation
8 Related Work and Conclusion
References
Dynamic Extrapolation in Extended Timed Automata
1 Introduction
2 Preliminary
2.1 Extended Timed Automata
2.2 Symbolic Semantics
2.3 M-Extrapolation in XTA
3 Dynamic Extrapolation
3.1 Reducing Relevant Paths
3.2 Dynamic LU-Extrapolation
3.3 A Note on Timed Automata Networks
4 Experiments and Results
5 Conclusion
References
Formalizing Robustness Against Character-Level Perturbations for Neural Network Language Models
1 Introduction
2 Related Work