Formal Methods: 24th International Symposium, FM 2021, Virtual Event, November 20–26, 2021, Proceedings

Preface
Organization
Contents
Invited Presentations
Combining Forces: How to Formally Verify Informally Defined Embedded Systems
	1 Introduction
	2 Related Work
	3 Preliminaries
		3.1 SystemC
		3.2 Simulink
	4 Transformation-Based Formalization
		4.1 Formalization of SystemC
		4.2 Formalization of Simulink
		4.3 Experimental Results with Single Verification Tools
	5 Combining Forces: Compositional Verification
		5.1 Combined Verification for SystemC
		5.2 Compositional Verification for Simulink
	6 Open Challenges
	7 Conclusion
	References
Model Checking for Verification of Quantum Circuits
	1 Introduction
	2 Quantum Logic Circuits
		2.1 Combinational Quantum Circuits
		2.2 Noisy Quantum Circuits
		2.3 Dynamic Quantum Circuits
		2.4 Sequential Quantum Circuits
		2.5 Quantum Transition Systems as a Model of Quantum Circuits
	3 Tensor Network Representation of Quantum Circuits
		3.1 Tensor Networks
		3.2 Representing Quantum States and Quantum Gates
		3.3 Representing Quantum Circuits
		3.4 Optimisations for Tensor Network Contraction
	4 Reachability Analysis of Quantum Circuits
		4.1 Adjacency and Reachability
		4.2 Computing Reachable Subspaces
	5 Temporal Quantum Logic
		5.1 Birkhoff-von Neumann Quantum Logic
		5.2 Computation Tree Quantum Logic
	6 Model Checking Quantum Circuits
		6.1 CTQL Model Checking
		6.2 Assertion-Based Verification of Quantum Circuits
	7 Conclusion
	References
Interactive Theorem Proving
Verifying Secure Speculation in Isabelle/HOL
	1 Introduction
	2 Transient Execution Vulnerabilities
		2.1 Spectre Variant 1: Bounds Check Bypass
		2.2 TPOD
	3 Operational Semantics
		3.1 Syntax and Semantics
		3.2 Adversary Model
		3.3 Formalising TPOD
	4 Mechanisation Techniques
		4.1 Program Specification
		4.2 Operational Semantics
		4.3 Program Execution
	5 Case Studies
	6 Related Work
	7 Conclusions
	References
Two Mechanisations of WebAssembly 1.0
	1 Introduction
	2 Wasm 1.0 Core Semantics
		2.1 Core Concepts
		2.2 Abstract Syntax
		2.3 Runtime Semantics
		2.4 Validation
	3 Wasm 1.0 Type Soundness
	4 Wasm 1.0 Full Semantics
	5 Related Work
	6 Conclusion and Future Work
	References
Neural Networks and Active Learning
Probabilistic Verification of Neural Networks Against Group Fairness
	1 Introduction
	2 Preliminary
	3 Our Approach
		3.1 Step 1: Learning a Markov Chain
		3.2 Step 2: Probabilistic Model Checking
		3.3 Step 3: Sensitivity Analysis
		3.4 Step 4: Improving Fairness
	4 Implementation and Evaluation
		4.1 Experiment Setup
		4.2 Research Questions and Answers
	5 Related Work
	6 Conclusion
	References
BanditFuzz: Fuzzing SMT Solvers with Multi-agent Reinforcement Learning
	1 Introduction
	2 Background on Reinforcement Learning
		2.1 Reinforcement Learning
		2.2 Satisfiability Modulo Theories
		2.3 Software Fuzzing
	3 BanditFuzz: A Multi-agent RL-Guided Performance Fuzzer
		3.1 The Performance Margin
		3.2 BanditFuzz: The Multi-agent RL-Based Fuzzing Algorithm
		3.3 The Original BanditFuzz Algorithm vs. The Current Version
	4 Implementation and Engineering
	5 Using the BanditFuzz Fuzzing Framework
		5.1 Using smtfuzz
		5.2 Using banditfuzz
	6 Empirical Evaluation
		6.1 Experimental Setup
		6.2 Results
	7 Case Studies with Solver Developers
		7.1 CVC4, Bitwuzla, and SymFPU
		7.2 Z3 String Solver
	8 Threats to Validity
	9 Related Work
	10 Conclusions
	References
Formally Verified Safety Net for Waypoint Navigation Neural Network Controllers
	1 Introduction
	2 Background
	3 Modeling the Waypoint Navigation Task
	4 Proving Safety
		4.1 Safe Starting States and Safe Actions
		4.2 Safe Region
		4.3 Safe Action
	5 Training a Neural Network Controller
		5.1 Controller Training
		5.2 Evaluating and Improving upon an Initial Controller
		5.3 Controller Safety
	6 Discussion
		6.1 Conclusions and Next Steps
		6.2 Brief Comparison to Related Work
	References
Model-Free Reinforcement Learning for Lexicographic Omega-Regular Objectives
	1 Introduction
	2 Preliminaries
	3 From Lexicographic Objectives to Learning in 3.5 Steps
		3.1 Lexicographic -regular Objectives
		3.2 Optimal Strategies for Lexicographic Objectives
		3.3 Outline of Our Reduction
		3.4 From Lexicographic Objectives to Lexicographic Büchi
		3.5 From Lexicographic Büchi to Weighted Büchi
		3.6 From Weighted Büchi to Weighted Reachability
		3.7 Wrapping Up Weighted Reachability
	4 Experimental Results
		4.1 Robot
		4.2 Computer Virus
		4.3 Human-in-the-Loop UAV Mission Planning
		4.4 Seven Bridges of Königsberg
	5 Conclusion
	References
Logics and Theory
Efficient Algorithms for Omega-Regular Energy Games
	1 Introduction
	2 An Illustrative Example
	3 Preliminaries
	4 Energy mu-Calculus Over Weighted Game Structures
	5 Evaluation
	6 Related Work
	7 Conclusion
	References
Generalizing Non-punctuality for Timed Temporal Logic with Freeze Quantifiers
	1 Introduction
	2 Preliminaries
	3 Introducing Non-adjacent 1-TPTL and PnEMTL
	4 Anchored Interval Word Abstraction
	5 1-TPTL to PnEMTL
	6 Satisfiability Checking for Non-adjacent PnEMTL
	7 Conclusion
	References
Verified Quadratic Virtual Substitution for Real Arithmetic
	1 Introduction
	2 Related Work
	3 The Virtual Substitution Algorithm
		3.1 Example
		3.2 Equality Virtual Substitution Algorithm
		3.3 General Virtual Substitution Algorithm
		3.4 Top Level Algorithms
	4 Framework
		4.1 Representation of Formulas
		4.2 Modified Disjunctive Normal Form
		4.3 Logical Evaluation
		4.4 Polynomial Contributions
	5 Experiments
	6 Conclusion and Future Work
	References
Business Processes Meet Spatial Concerns: The sBPMN Verification Framework
	1 Introduction
	2 Formal Semantics
		2.1 Formal Models for Space BPMN
		2.2 Semantics for Space BPMN: States and Initial State
		2.3 Semantics for Space BPMN: Formulas and Actions
		2.4 Semantics for Space BPMN: Execution Semantics
	3 Implementation and Verification
		3.1 Implementing the Semantics and Encoding Models in TLA+
		3.2 Properties and Verification
		3.3 Experiments
	4 Related Work
	5 Conclusion and Perspectives
	References
Program Verification I
Owicki-Gries Reasoning for C11 Programs with Relaxed Dependencies
	1 Introduction
	2 MRD and Semantic Dependencies
	3 Operational Semantics with Relaxed Write Propagation
	4 Operational Semantics over MRD
		4.1 Program Futures
		4.2 Future-Based Transition Relation
		4.3 Example
	5 Hoare Logic and Owicki-Gries Reasoning
	6 A Verification Example
		6.1 View-Based Assertions
		6.2 Example Proof
	7 Related Work
	8 Conclusions and Future Work
	References
Integrating ADTs in KeY and Their Application to History-Based Reasoning
	1 Introduction
	2 Integrating Abstract Data Types in KeY
	3 Case Study: History-Based Reasoning About Collection
		3.1 Significant Improvement in Proof Effort
		3.2 Advanced Use Cases
	4 Conclusion
	References
Identifying Overly Restrictive Matching Patterns in SMT-Based Program Verifiers
	1 Introduction
	2 Overview
	3 Synthesizing Triggering Terms
		3.1 Input Formula
		3.2 Algorithm
		3.3 Limitations
	4 Evaluation
		4.1 Effectiveness on Verification Benchmarks with Triggering Issues
		4.2 Effectiveness on SMT-COMP Benchmarks
		4.3 Comparison with Unsatisfiability Proofs
	5 Related Work
	6 Conclusions
	References
Rely/Guarantee Reasoning for Multicopy Atomic Weak Memory Models
	1 Introduction
	2 Preliminaries
		2.1 Rely/Guarantee Reasoning
	3 Weak Memory Models
		3.1 Reordering Semantics
		3.2 Reordering Interference Freedom
		3.3 Computing All Reorderable Instructions
		3.4 Interference Checking
		3.5 Elimination of Reordering Interference
		3.6 Soundness
		3.7 Completeness
	4 Instantiating the Proof System
		4.1 Peterson\'s Mutual Exclusion Algorithm
	5 Conclusion
	References
Hybrid Systems
Hybrid System Falsification for Multiple-Constraint Parameter Synthesis: A Gas Turbine Case Study
	1 Introduction
		1.1 Parameter Synthesis for Power Plants
		1.2 Previous Approaches
		1.3 Hybrid System Falsification as Logic-Guided Metaheuristics
		1.4 Encountered Challenges and Countermeasures
		1.5 Experience and Lessons
	2 Our Problem: Synthesis of Gas Turbine Parameters Under Multiple Constraints
		2.1 The Target Gas Turbine Model
		2.2 Requirements
	3 Synthesis by Optimization-Based Falsification
		3.1 Signal Temporal Logic (STL)
		3.2 Optimization-Based Falsification
		3.3 Application to Our Synthesis Problem, and Challenges Therein
	4 Falsification with MCR and the Area Modality
		4.1 Multiple Constraint Ranking (MCR) for Conjunctive Synthesis
		4.2 Area Modality for Spatial and Temporal Robustness
	5 Experimental Evaluation
		5.1 Approach 1: Manual
		5.2 Approach 2: Breach
		5.3 Approach 3: MCR+Area with an Empirical Initial Valuation (MCR+Areaw)
		5.4 Approach 4: MCR+Area without Empirical Initial Valuation (MCR+Areawo)
	6 Conclusions and Future Work
	References
Gaussian Process-Based Confidence Estimation for Hybrid System Falsification
	1 Introduction
	2 Background
	3 Problem Definition and Overview of the Proposed Approach
	4 Confidence Estimation via Gaussian Process Regression
		4.1 Building a Surrogate Model of the Robustness Function via Gaussian Process Regression
		4.2 Confidence Estimation
	5 Experimental Evaluation
		5.1 Experiment Settings
		5.2 Evaluation
	6 Related Work
	7 Conclusion
	References
Formal Verification of Intelligent Hybrid Systems that are Modeled with Simulink and the Reinforcement Learning Toolbox
	1 Introduction
	2 Preliminaries
		2.1 Reinforcement Learning
		2.2 Simulink and the RL Toolbox
		2.3 Differential Dynamic Logic
		2.4 Simulink2dL Transformation and Hybrid Contracts
	3 Related Work
	4 Our Approach for Verifying Intelligent Hybrid Systems
		4.1 Running Example: Autonomous Intelligent Robot in a Factory
		4.2 Defining the Safe Behavior of RL Agents with Hybrid Contracts
		4.3 Transforming Safe RL Agents to dL
		4.4 Enforcing the Safe Behavior of RL Agents
	5 Evaluation
		5.1 Case Study of an Autonomous Robot in a Factory
		5.2 Collision Freedom with Additional Opponents
		5.3 Collision Freedom with Additional Sensor Disturbances
		5.4 Simulation Experiments
	6 Conclusion
	References
Hybrid Systems Verification with Isabelle/HOL: Simpler Syntax, Better Models, Faster Proofs
	1 Introduction
	2 Semantic Preliminaries
	3 Hybrid Store Components
	4 Shallow Expressions Component
	5 Dynamical Systems Components
	6 Reasoning Components
	7 Examples
	8 Related Work, Conclusions, and Future Work
	References
Program Verification II
Z3str4: A Multi-armed String Solver
	1 Introduction
	2 Formal Background
		2.1 Logical Theory TS
	3 Z3str4 Components and Architecture
		3.1 Novel Solver Algorithms in Z3str4
		3.2 Algorithm Selection and Clause Sharing
	4 Performance Evaluation
		4.1 Overall Evaluation
		4.2 Performance Analysis of Components of Z3str4
	5 Related Work
	6 Conclusion and Future Work
	References
Concise Outlines for a Complex Logic: A Proof Outline Checker for TaDA
	1 Introduction
	2 Running Example and TaDA Overview
		2.1 Regions and Atomicity
		2.2 TaDA Proof Outline
		2.3 Voila Proof Outline
	3 Proof Outline Language
	4 Proof Workflow
	5 Expanding Proof Outlines to Proof Candidates
	6 Validating Proof Candidates in Viper
	7 Evaluation
	8 Related Work
	9 Conclusion
	References
Formal Verification of a JavaCard Virtual Machine with Frama-C
	1 Introduction
	2 Frama-C Verification Platform
	3 Overview of JavaCard Virtual Machine
	4 Memory Modeling and Companion Ghost Model
	5 Predicates, Lemmas and Scripts
	6 Verification of Security Properties with MetAcsl
	7 Specification Architecture and Effort
	8 Proof Results and Lessons Learned
		8.1 Proof Results
		8.2 Lessons Learned
	9 Related Work
	10 Conclusion
	References
Verification of the Incremental Merkle Tree Algorithm with Dafny
	1 Introduction
	2 Incremental Merkle Trees
	3 Recursive Incremental Merkle Tree Algorithm
	4 Verification of the Algorithms
	5 Findings and Lessons Learned
	References
Automata
Congruence Relations for Büchi Automata
	1 Introduction
	2 Preliminaries
	3 Improved Congruence Relations for NBAs
		3.1 Classical Congruence Relations
		3.2 Improved Congruence Relations for NBAs
	4 Optimal Congruence Relations for NBAs
	5 Connection to FDFAs
	6 Concluding Remarks
	References
Featured Team Automata
	1 Introduction
	2 Variability
	3 Team Automata with Variability
		3.1 Featured Component Automata and Featured Systems
		3.2 Featured Team Automata
		3.3 fETA Versus ETA
	4 Receptiveness
		4.1 Receptiveness for ETA
		4.2 Featured Receptiveness for fETA
		4.3 From Featured Receptiveness to Receptiveness
	5 Tool Support
	6 Conclusion
	References
From Partial to Global Assume-Guarantee Contracts: Compositional Realizability Analysis in FRET
	1 Introduction
	2 Liquid Mixer System Example
	3 Background on Realizability
		3.1 Assume-Guarantee (AG) Contracts
		3.2 Realizability
	4 Decomposing Realizability
	5 Connected Components
	6 Case Studies
		6.1 Analysis Outcomes and Lessons Learned
		6.2 Comparison of Decomposition with Finkbeiner et al. ch27finkbeiner2021specification
	7 Related Work
	8 Conclusion
	References
Fingerprinting Bluetooth Low Energy Devices via Active Automata Learning
	1 Introduction
	2 Preliminaries
		2.1 Mealy Machines
		2.2 Active Automata Learning
		2.3 Bluetooth Low Energy
	3 Learning Setup
	4 Evaluation
		4.1 BLE Devices
		4.2 BLE Learning
		4.3 BLE Fingerprinting
	5 Related Work
	6 Conclusion
	References
Analysis of Complex Systems
Trace Abstraction-Based Verification for Uninterpreted Programs
	1 Introduction
	2 Background and Illustration
		2.1 Uninterpreted Programs
		2.2 Trace Abstraction Based CEGAR
	3 Verification Framework
		3.1 Congruence-Based Feasibility Checking
		3.2 Trace Abstraction
	4 Evaluation
		4.1 Effectiveness & Efficiency
		4.2 The Results of Different Trace Abstraction Methods
		4.3 The Results on SV-COMP Benchmark
	5 Conclusion and Future Work
	References
HStriver: A Very Functional Extensible Tool for the Runtime Verification of Real-Time Event Streams
	1 Introduction
	2 The HStriver Tool
		2.1 How to Run HStriver
	3 Example Specifications and Libraries
		3.1 Example: Clock
		3.2 Libraries
		3.3 STL
		3.4 Example: Cost Computation
		3.5 Example: PowerTrain
		3.6 Example: Smart Home
	4 Conclusion
	References
Cabean 2.0: Efficient and Efficacious Control of Asynchronous Boolean Networks
	1 Introduction
	2 Related Work
	3 Preliminaries
	4 Functionalities
	5 Evaluation
	6 Implementation
	7 Conclusion
	References
Dynamic Reconfiguration via Typed Modalities
	1 Introduction
	2 Membrane Budding
	3 Logical Support for Dynamic Networks of Interactions
	4 A Proof-by-translation Technique for  DNI
	5 Conclusions
	References
Probabilities
On Lexicographic Proof Rules for Probabilistic Termination
	1 Introduction
	2 Mathematical Preliminaries
	3 Generalized Lexicographic Ranking Supermartingales
	4 Program-Specific Preliminaries
	5 GLexRSMs for Probabilistic Programs
	6 Algorithm for Linear Probabilistic Programs
		6.1 Linear Programs with Distributions of Bounded Support
		6.2 Algorithm for General LinPPs
	7 Conclusion
	References
Fuel in Markov Decision Processes (FiMDP): A Practical Approach to Consumption
	1 Introduction
	2 Consumption Markov Decision Processes
	3 Features of FiMDP
		3.1 Theoretical Foundations
		3.2 New Features
	4 FiMDP: What Is Under the Hood and How to Drive It
	5 FiMDPEnv: Environments for FiMDP
		5.1 UUV Environment
		5.2 AEV Environment
	6 Evaluation
		6.1 Analyzing CMDPs in FiMDP and Storm
		6.2 Goal-Leaning Solvers
		6.3 Multi-agent Allocation
	7 Conclusion
	References
HyperProb: A Model Checker for Probabilistic Hyperproperties
	1 Introduction
	2 Input to the Tool
	3 Tool Structure and Usage
		3.1 Implementation
		3.2 Usage
	4 Evaluation
		4.1 Case Studies
		4.2 Results and Discussions
	5 Conclusion
	References
The Probabilistic Termination Tool Amber
	1 Introduction
	2 Usage and Components
	3 Evaluation
	4 Conclusion
	References
Model Checking Collision Avoidance of Nonlinear Autonomous Vehicles
	1 Introduction
	2 Problem Description
	3 Definitions and Verification Reduction Theorems
		3.1 Definitions of Maps, Agent States, and Trajectories
		3.2 Collision-Avoidance Verification Reduction
		3.3 Discretization of Trajectories
	4 Verification Approach and Tool Support
		4.1 General Description of the Approach
		4.2 Design of the UTA Templates and CTL Properties
		4.3 Reduction of the State Space of the UTA Model
	5 Experimental Evaluation
		5.1 The Collision-Avoidance Algorithm to Be Verified
		5.2 Verification Results
	6 Related Work
	7 Conclusion and Future Work
	References
Industry Track Invited Papers
Formal Verification of Complex Data Paths: An Industrial Experience
	1 Introduction
	2 Technology
		2.1 Symbolic Representations
		2.2 Model Checking
		2.3 Theorem Proving
		2.4 Specifications
	3 Tools
		3.1 Model Import
		3.2 Scripting and Implementation Language
		3.3 Specification Language
		3.4 Term Language
		3.5 Visualization
	4 Methodology
		4.1 Wiggling
		4.2 Scalar Verification
		4.3 Symbolic Verification
		4.4 Theorem Proving
		4.5 Regression
	5 Examples
		5.1 Floating Point Unit
		5.2 Complete Micro-controller ISA Verification
	6 Discussion
	References
Some Lessons Learned in the Industrialization of Formal Methods for Financial Algorithms
	1 Extended Abstract
	References
Industry Track
Two Decades of Formal Methods in Industrial Products at BTC Embedded Systems
	1 Introduction
	2 Formal Methods in BTC Products
	3 Conclusion
	References
Formal Analysis of Neural Network-Based Systems in the Aircraft Domain
	1 Introduction
	2 Network Verification with the Venus Toolkit
	3 Neural Network-Based Systems for the Aircraft Domain
		3.1 Object Detection with Open Categories
		3.2 Collision Avoidance for Landing at Non-towered Airports
	4 Conclusions and Outlook
	References
Formal Verification of Consensus in the Taurus Distributed Database
	1 Introduction
	2 Taurus Distributed Database
	3 Approach
		3.1 Specifying the System with TLA+
		3.2 Properties of Interest
		3.3 Model Checking with TLC
		3.4 Fault Injection Analysis
		3.5 Theorem Proving with TLAPS
	4 Lessons and Challenges
		4.1 Total Effort
		4.2 Why TLA+ Was Chosen
		4.3 Challenges and Limitations
	5 Related Work
		5.1 Formal Verification of Distributed Protocols
		5.2 Verifying Distributed Systems Using TLA+
	6 Conclusion
	References
Combined Online Checking and Control Synthesis: A Study on a Vehicle Platoon Testbed
	1 Introduction
	2 Robotic Vehicle Testbed and Platoon Scenario
		2.1 Robotic Vehicle Testbed
		2.2 Vehicle Platoon Scenario
	3 Periodically Online Safety Assurance Framework
		3.1 Online Modeling
		3.2 Combined Online Verification and Control Synthesis
		3.3 Assignment Scheduling
	4 Deployment and Evaluations
		4.1 Framework Deployment
		4.2 Framework Evaluation
	5 Related Work
	6 Conclusion
	References
Formally Guaranteed Tight Dynamic Future Occupancy of Autonomous Vehicles
	1 Introduction
	2 Problem Definition
		2.1 Vehicle Model
	3 Motion Primitives
	4 Motion Primitive Matching
	5 Examples
	6 Conclusion
	References
Divide et Impera: Efficient Synthesis of Cyber-Physical System Architectures from Formal Contracts
	1 Introduction
	2 Background
	3 Methodology
	4 Encodings
	5 Evaluation
	6 Related Work
	7 Conclusions and Future Work
	References
Apply Formal Methods in Certifying the SyberX High-Assurance Kernel
	1 Introduction
	2 SyberX
	3 Methodology in Isabelle/HOL
		3.1 Specifications
		3.2 Verification
	4 Application to the SyberX Kernel
		4.1 Security Target
		4.2 Formalizing Specification
		4.3 Verification
		4.4 Results
	5 Discussion and Conclusion
	References
Author Index