Integrated Formal Methods: 17th International Conference, IFM 2022, Lugano, Switzerland, June 7–10, 2022, Proceedings

Preface
Organization
Side Channel Secure Software (Abstract of Invited Talk)
Contents
Invited Presentations
Verifying Autonomous Systems
	1 Introduction
	2 A Cognitive Agent Decision Maker
	3 Verifying Autonomous Choices
		3.1 The MCAPL Framework
	4 The Problem with Environments
	5 Compositional Verification
		5.1 Module Level vs. System Level Properties
		5.2 Combining Results
	6 Conclusion
	References
Empowering the Event-B Method Using External Theories
	1 Introduction
	2 Invariants and Well-Definedness (WD)
	3 Overview of Event-B
		3.1 Contexts and Machines (Tables1b and 1c)
		3.2 Event-B Extensions with Theories
	4 An Illustrative Case Study
	5 Invariant Preservation: Core Event-B
	6 Data Type Theory-Based Invariant Preservation
		6.1 An Event-B Datatype Based Domain-Specific Theory (Step 1)
		6.2 An Event-B Instantiation Context (Step 2)
		6.3 A Domain-Specific Event-B Machine (Step 3)
	7 The Proof Process
	8 Revisited Event-B Models for LTS
		8.1 A Data Type for LTS (Step 1)
		8.2 An Instanciation Context for LTS (Step 2)
		8.3 A Data Type Specific Machine for LTS (Step 3)
		8.4 Proof Process
	9 Conclusion
	References
Cooperative and Relational Verification
Journal-First: Formal Modelling and Runtime Verification of Autonomous Grasping for Active Debris Removal
	1 Introduction
	2 Summary
		2.1 Verification Approaches
		2.2 Gaps in the Requirements
		2.3 Post-implementation Verification
	3 Conclusions and Future Work
	References
Formal Specification and Verification of JDK\'s Identity Hash Map Implementation
	1 Introduction
	2 Preliminaries
	3 The Verification Subject: JDK\'s IdentityHashMap
	4 Specification and Verification of the IdentityHashMap
		4.1 Mechanic Proof
	5 Engineering Specifications Using Lightweight Analyses
		5.1 Bounded Analysis for Auxiliary Specifications
		5.2 Unit Tests for Property Specifications
	6 Discussion
		6.1 Empirical Identification of Verification Challenges
		6.2 Discovered Bugs and Recommendations
	7 Conclusion
	References
Reusing Predicate Precision in Value Analysis
	1 Introduction
	2 Programs and Precisions
	3 From Predicate Precision to Initial Value Precision
	4 Evaluation
		4.1 Experimental Setup
		4.2 Experimental Results
	5 Related Work
	6 Conclusion
	References
Certified Verification of Relational Properties
	1 Introduction
	2 Syntax and Semantics of the L Language
		2.1 Notation for Locations, States, and Procedure Contracts
		2.2 Syntax for Expressions and Commands
		2.3 Operational Semantics
	3 Functional Correctness
	4 Relational Properties
	5 Verification Condition Generation for Hoare Triples
		5.1 Verification Condition Generator
		5.2 Hoare Triple Verification
	6 Verification of Relational Properties
	7 Related Work
	8 Conclusion
	References
B Method
Reachability Analysis and Simulation for Hybridised Event-B Models
	1 Introduction
	2 The State-Of-The-Art in CPS V&V
	3 Framework for CPS Design and Analysis
	4 Preliminaries
		4.1 Event-B and Hybridised Event-B
		4.2 Reachability Analysis and JuliaReach
		4.3 Simulink and Stateflow
	5 Case Study: Railway Signalling System
		5.1 Continuous Rolling Stock Model
		5.2 Communication-Based Railway Signalling Model
	6 Case Study: Formal Development
		6.1 Event-B Model Development and Verification
		6.2 Train Model Simulation and Validation
	7 Conclusions and Future Work
	References
Operation Caching and State Compression for Model Checking of High-Level Models
	1 Introduction
	2 Current State of Model Checking for B
		2.1 Prolog Default Model Checker
		2.2 TLC Backend
		2.3 LTSMin Backend
	3 Compression and Other Improvements
		3.1 Timeouts
		3.2 Reducing Stored Transitions
		3.3 State Compression
	4 Operation Caching
	5 Experiments
	6 Discussion and Conclusion
	References
Time
Conservative Time Discretization: A Comparative Study
	1 Introduction
	2 Problem Statement
	3 Discretization Methods
		3.1 Notation
		3.2 Methods for Nonlinear Systems
		3.3 Common Structure of Methods for Linear Systems
		3.4 First-Order d/dt Method
		3.5 First-Order Zonotope Method
		3.6 Correction-Hull Method
		3.7 First-Order Method
		3.8 Forward-Backward Method
		3.9 Forward-Only Method
		3.10 Combining Methods
		3.11 Application to High-Dimensional Systems
		3.12 Application to Time-Varying Systems
	4 Problem Transformations
		4.1 Homogenization
		4.2 Shrinking the Time Step
	5 Efficient Implementation
		5.1 The Concept of a Lazy Set
		5.2 Computation of Matrix Functions
		5.3 Simplification of the Set Representation
	6 Experimental Evaluation
		6.1 Setup
		6.2 Models
		6.3 Visual Evaluation of Varying Parameters
		6.4 Quantitative Evaluation by Scaling
		6.5 Summary
	7 Conclusion
	References
Untangling the Graphs of Timed Automata to Decrease the Number of Clocks
	1 Introduction
	2 Timed Automata
	3 Constructing a Better Automaton
		3.1 Building a Tree from a Timed Automaton
		3.2 Untangling Trees: An Overview
		3.3 Step One: Computing the Real Cost and Group Analysis
		3.4 Step Two: Untangling
		3.5 Obtaining the Final Automaton
	4 Implementation and Experimental Results
	5 Stepping Outside TAS
	6 Conclusions
	References
Probability
Probabilistic Model Checking of BPMN Processes at Runtime
	1 Introduction
	2 Models
	3 Probabilistic Model Checking of BPMN
		3.1 Overview
		3.2 BPMN Process Monitoring
		3.3 Transforming LTS into PTS
	4 Tool Support
		4.1 Tool
		4.2 Case Study
		4.3 Additional Experiments for Performance Evaluation
	5 Related Work
	6 Conclusion
	References
HyperPCTL Model Checking by Probabilistic Decomposition
	1 Introduction
	2 Preliminaries
		2.1 HyperPCTL Syntax
		2.2 HyperPCTL Semantics
	3 A Probabilistic Decomposition Approach
	4 Probabilistically Dependent Markov Chains
		4.1 Time and Memory Complexity
	5 Case Studies and Evaluation
	6 Conclusion and Future Work
	References
Learning and Synthesis
Learning Finite State Models fromRecurrent Neural Networks
	1 Introduction
	2 Preliminaries
	3 Automata Extraction from RNNs
		3.1 Test-Based Learning from RNNs
		3.2 Equivalence Queries from a Practical Perspective
		3.3 Research Questions
	4 Experiments on Learning Automata from RNNs
		4.1 Learning Models of RNNs Trained on Tomita Grammars
		4.2 Learning Models of RNNs Trained on Balanced Parentheses
		4.3 Analyzing RQ2 on the Tomita 3 Grammar
	5 Related Work
	6 Conclusion
	References
Kaki: Concurrent Update Synthesis for Regular Policies via Petri Games
	1 Introduction
	2 Concurrent Update Synthesis
		2.1 Routing Policy
		2.2 Concurrent Update Synthesis Problem
	3 Optimisation Techniques
		3.1 Topological Decomposition
		3.2 Collective Update Classes
	4 Translation to Petri Games
		4.1 Petri Games
		4.2 Translation Intuition
		4.3 Translation of Network Topology and Routings
		4.4 Policy Translation
		4.5 Reachability Objective and Translation Correctness
	5 Experimental Evaluation
		5.1 Results
	6 Conclusion
	References
Security
Verified Password Generation from Password Composition Policies
	1 Introduction
	2 Current Password Generation Algorithms
		2.1 Password Composition Policies
		2.2 Random Password Generation
	3 Verified Password Generation
		3.1 Reference Implementation
		3.2 Formal Proofs
	4 Case Study: From Apple Password Rules to Verified Password Generation in Bitwarden
		4.1 Apple\'s Password Autofill Rules
		4.2 Jasmin Password Generator
		4.3 Integration with Bitwarden
	5 Related Work
	6 Conclusion
	References
A Policy Language to Capture Compliance of Data Protection Requirements
	1 Introduction
	2 Main Principles of the GDPR
	3 A Policy Language for Main Data Protection Principles
	4 Taxonomies as Tree Structures
	5 Policy Compliance
	6 Proof of Concept Implementation
	7 Case Study: Health Wearable
	8 Analysis of Related Work
	9 Conclusion and Future Work
	References
Static Analysis and Testing
Extending Data Flow Coverage to Test Constraint Refinements
	1 Introduction
	2 Motivation Examples
	3 Background
	4 The Required k-Use Chains
	5 Related Work and Conclusions
	References
Scalable Typestate Analysis for Low-Latency Environments
	1 Introduction
	2 Bit-Vector Typestate Analysis
		2.1 Annotation Language
		2.2 Bit-Vector Finite Automata
	3 Compositional Analysis Algorithm
	4 Evaluation
	5 Related Work
	6 Concluding Remarks
	References
PhD Symposium Presentations
Studying Users\' Willingness to Use a Formally Verified Password Manager
	1 Introduction
	2 Current Work
		2.1 First Study
		2.2 Second Study
	3 Conclusion and Impact
	References
Modeling Explanations in Autonomous Vehicles
	1 Introduction
	2 Related Work and Current Progress
	3 Conclusion and Future Work
	References
A Requirements-Driven Methodology: Formal Modelling and Verification of an Aircraft Engine Controller
	1 Overview
	2 Three-Phase Methodology
	3 `FRET-Guided\' Modelling
	4 Future Work
	References
A Dialogue Interface for Low Code Program Evolution
	1 Introduction
	2 Approach
	3 Conclusions
	References
Simple Dependent Types for OSTRICH
	1 Introduction
	2 Approach
	3 Conclusions
	References
SNITCH: A Platform for Information Flow Control
	1 Introduction
	2 Approach
	3 Conclusion
	References
Machine-Assisted Proofs for Institutions in Coq
	1 Introduction
	2 Mathematical Background and Contributions
	3 Conclusions and Future Work
	References
Author Index