Leveraging Applications of Formal Methods, Verification and Validation. Specification and Verification 12th International Symposium, ISoLA 2024, Proceedings, Part III

Preface
Organization
Contents – Part III
Specify This
SpecifyThis Bridging Gaps Between Program Specification Paradigms: Track Introduction
	1 Introduction
	2 Contributions
	References
Deductively Verified Program Models for Software Model Checking
	1 Introduction
	2 Deductive Verification Based Program Abstraction
	3 Annotated Programs and Flow Graphs
		3.1 Annotated Programs
		3.2 Flow Graphs
	4 From Annotated Programs to Flow Graphs
	5 Model Checking of Flow Graphs
		5.1 Model Checking with TLC
		5.2 Model Checking with nuXmv
	6 Discussion
	7 Conclusion
	A Full TLA+ and nuXmv Model of Stee
		A.1 TLA+ Model
		A.2 nuXmv model
	References
Towards Probabilistic Contracts for Intelligent Cyber-Physical Systems
	1 Introduction
	2 Existing Modeling and Evaluation Approaches
		2.1 Contracts-Based Design and Verification
		2.2 Formal Verification of Hybrid Systems
		2.3 Model-Based Evaluation in the Presence of Uncertainty
	3 Sources of Uncertainties in Intelligent CPSes
	4 Towards Probabilistic Contracts
		4.1 Employing Behavior Distributions Instead of Behavior Sets as Assumptions and Guarantees
		4.2 Subdistributions in Assumptions and Guarantees
		4.3 Normalized Subdistribution Contracts
	5 An Example of a Subdistribution Contract
	6 Conclusion
	References
Towards the Formal Analysis of Algorithmic Requirements
	1 Introduction
	2 ERTMS and SDM
		2.1 The European Rail Traffic Management System
		2.2 The Speed and Distance Monitoring Function
	3 Implementing the ERA Subset
		3.1 An Inefficient Development Process
		3.2 Implementation Details and Results
		3.3 The MRSP Computation
	4 Formalizing the Requirements
	5 Validating the Requirements
	6 Implementation
	7 Conclusions
	References
Interest Beyond Violation: On Points-of-Interest in Runtime Verification
	1 Introduction
	2 Point and Temporal Properties
	3 On Norms
	4 Use Cases
		4.1 Underwater Robots
		4.2 Fraud Detection
	5 Conclusions
	References
Contract-LIB: A Proposal for a Common Interchange Format for Software System Specification
	1 Introduction
	2 Contract-LIB Overview and Motivating Examples
		2.1 High-Level Design and Ingredients
		2.2 Example: Linked List Specifications in Different Languages
	3 Technical Realization of Contract-LIB
		3.1 Syntax
		3.2 Semantics of Contracts
		3.3 Integration with Dynamic Frames and Separation Logic
		3.4 Standardized Theories and Polymorphism
		3.5 Partiality of Functions
	4 Pragmatics of Tool Integration
	5 Modeling Memcached in Dafny and Contract-LIB
		5.1 Data Model of memcached
		5.2 Memcached as a Well-Encapsulated Stateful Module
		5.3 Modeling Dynamic Behaviors of memcached Operations
	6 Related Work
	7 Outlook: Use Cases for Contract-LIB
	8 Conclusion
	References
Adventures in FRET and Specification
	1 Introduction
	2 Background
		2.1 FRET
		2.2 Event-B
		2.3 Dafny
		2.4 ROSMonitoring
	3 Case Studies
		3.1 Case Study 1 Aircraft Engine Controller
		3.2 Case Study 2 Mechanical Lung Ventilator
		3.3 Case Study 3 Inspection Rover
		3.4 Case Study 4 Autonomous Grasping
	4 Formalising and Specifying Requirements
		4.1 Requirement Metrics
		4.2 Specifying Using FRETish and Event-B
		4.3 Specification: FRET to Dafny
		4.4 Specification: FRET to Temporal Logic
		4.5 VerifyThis and DownSampling Point Clouds
	5 Discussion
	6 Conclusion
	References
Challenges of Multilingual Program Specification and Analysis
	1 Introduction
	2 Dimensions of Multilingual Programming
		2.1 Multilingual Program Levels
		2.2 Analysis and Specification Layers
	3 Examples of Multilingual Analysis and Specification
		3.1 API Level
		3.2 IR Level
		3.3 Native Level
		3.4 System Level
	4 Multilingual Analysis: State of the Art
		4.1 Language-Agnostic Multilingual Analysis
		4.2 Language-Specific Multilingual Analysis
	5 Discussion
	References
Towards Integrating Copiloting and Formal Methods
	1 Introduction
	2 Language Servers
	3 Tooling for Verification-Aware Languages
		3.1 Dafny
		3.2 Ada/SPARK
	4 Tooling for General Purpose Languages
		4.1 Frama-C
		4.2 KeY
	5 Interactive Theorem Provers
		5.1 Coq
		5.2 Lean
		5.3 The Direction of ITPs
	6 Copilots
		6.1 The Design Space of Github Copilot
		6.2 Build Your Own Copilot with Continue
		6.3 Fine-Tuning Models with Unsloth
	7 Takeaways
		7.1 LSP-based IDE Extensions
		7.2 Consolidation of Tools
		7.3 LLM-based Copilots for Formal Methods
		7.4 Datasets are Key
		7.5 Open Source Experimentation
	References
High-Level Program Properties in Frama-C: Definition, Verification and Deduction
	1 Introduction
	2 High-Level Program Properties: Motivation
	3 Definition of High-Level Properties Using Meta-properties
	4 Verification of High-Level Properties via Translation Into Low-Level Annotations
	5 Deduction of High-Level Properties: Initial Ideas and First Attempts
	6 Related Work
	7 Conclusion
	References
Formal Foundations of Consistency in Model-Driven Development
	1 Introduction
	2 The V-SUM Approach in Model-Driven Development
	3 Related Work
	4 Motivating Examples
		4.1 Linear Temporal Logic and Büchi Automata
		4.2 A Model-Driven Description of a Car\'s Brake System
	5 Set-Theoretic Foundations of the V-SUM Approach
	6 Defining V-SUM Consistency from Rules
		6.1 Model Transformation
		6.2 Rule-Based Consistency
	7 Defining V-SUM Consistency from Semantics
		7.1 An Abstract Semantics
		7.2 The Lattice of Semantics
		7.3 Semantics-Induced Consistency
		7.4 Consistency-Induced Semantics
	8 Conclusion
	References
Context-Aware Contracts as a Lingua Franca for Behavioral Specification
	1 Introduction
	2 Need for a Lingua Franca for Behavioral Specification
	3 CATs as a Lingua Franca for Behavioral Specification
		3.1 Trace Formulas
		3.2 What is a CAT?
		3.3 Domain-Specific Specification
		3.4 CATs as a Lingua Franca for Behavioral Specification
	4 The Casino Case Study in JML
		4.1 The Casino Case Study
		4.2 JML Specification of Casino Case Study
	5 Desugaring JML to CATs
		5.1 Desugaring State-Based Properties
		5.2 Ghostbusting JML
	6 Related Work
	7 Conclusion and Future Work
	References
SIMPPAAL: A Framework for Statistical Model Checking of Industrial Simulink Models
	1 Introduction
	2 Preliminaries
		2.1 Simulink
		2.2 UPPAAL SMC
	3 Simulink to UPPAAL SMC: Approach
		3.1 Formal Definitions
		3.2 STA Patterns
		3.3 Flattening Algorithm for Preserving the Execution Order
		3.4 Proof of Transformation Soundness
	4 SIMPPAAL Tool
	5 Application on Brake-by-Wire Use Case
	6 Related Work
	7 Conclusions and Future Work
	References
Static and Dynamic Verification of OCaml Programs: The Gospel Ecosystem
	1 Introduction
	2 The Gospel Ecosystem, in a Nutshell
		2.1 Gospel – A Specification Language for OCaml
		2.2 Ortac – Runtime Assertion Checking of OCaml Programs
		2.3 Cameleer – Auto-active Verification of OCaml Programs
		2.4 CFML – Interactive Verification of OCaml Programs
	3 Certification Workflow
	4 Case Study: Path Checking in a Graph
		4.1 Implementation
		4.2 Dynamic Analysis of Auxiliary Data Structures, in Ortac
		4.3 Path Checking Proof, in Cameleer
		4.4 Proof of Auxiliary Data Structures, in CFML
	5 Related Work
	6 Conclusions and Future Work
	A COMPARABLE Module Signature
	B Queue Specification for Ortac
	References
Scalable Verification and Validation
Scalable Verification and Validation of Concurrent and Distributed Systems (ScaVeri) (Track Summary)
	1 Motivation and Goals
	2 Overview of Contributions
	References
SyDPaCC: A Framework for the Development of Verified Scalable Parallel Functional Programs
	1 Introduction
	2 An Overview of Coq
	3 SyDPaCC by Example
		3.1 Trusted Base
	4 SyDPaCC Behind the Scenes
		4.1 Reasoning About Functional Bulk Synchronous Parallel Programs
		4.2 Program Transformations
	5 A Tour of SyDPaCC Transformations and Applications
	6 Related Work
	7 Conclusion and Future Work
	References
A Theory of Probabilistic Contracts
	1 Introduction
	2 Contract Metatheory for I/O Systems
		2.1 Syntax
		2.2 Semantics
	3 Probabilistic Contract Theory
		3.1 Traces and Behaviors
		3.2 Probabilistic Instantiation of the Metatheory
		3.3 Independence
	4 Deductive System
	5 Illustrative Example
		5.1 Requirements Decomposition
		5.2 Domain Knowledge
		5.3 Verifying the Requirements Decomposition
	6 Conclusion
	A Proofs of Correctness for the Inference Rules
	B Refinement Proof
	References
Composition and Merging of Assume-Guarantee Contracts Are Tensor Products
	1 Introduction
	2 Assume-Guarantee Contracts
		2.1 Conjunction and Disjunction
		2.2 Axioms for Composition and Merging
	3 Tensor Products of Contracts
		3.1 Tensor Products of Bimodules over Monoids
		3.2 The Tensor Product of Conjunctive Monoids of Contracts
		3.3 The Tensor Product of Disjunctive Monoids of Contracts
	4 Discussion and Concluding Remarks
	References
Avoiding Distractions in Parity Games
	1 Introduction
	2 Preliminaries
	3 Tangle Learning
	4 Recursive Tangle Learning
	5 Empirical Evaluation
		5.1 Setup
		5.2 Results
	6 Discussion
	A Optimizations
	References
No Need to Be Stubborn: Partial-Order Reduction for GPU Model Checking Revisited
	1 Introduction
	2 Preliminaries
	3 Partial-Order Reduction in GPUexplore 3.0
		3.1 Ample Sets
		3.2 Clustered-Ample Sets
		3.3 Stubborn Sets
	4 Experiments
	5 Related Work
	6 Conclusions and Future Work
	References
SAT-Based Quantified Symmetric Minimization of the Reachable States of Distributed Protocols: An Update
	1 Introduction
	2 Quantified Symmetric Minimization: The QSM Procedure
	3 The Update
		3.1 Optimizing Step 1: Symmtery-Aware Depth-First Search
		3.2 Refining Step 2: Super Orbits
		3.3 Refining Step 2: Unbounded Orbits
		3.4 Optimizing Step 4: Better Coverage Estimation in Set Covering
		3.5 Where is Cutoff?
	4 Conclusions
	A Minimum Reachable Formulas for Protocols without Quorums
	B Minimum Reachable Formulas for Protocols with Quorums
	References
CommonUppRoad: A Framework of Formal Modelling, Verifying, Learning, and Visualisation of Autonomous Vehicles
	1 Introduction
	2 Preliminaries
		2.1 UPPAAL, Timed Games, and Decision Trees
		2.2 CommonRoad
	3 Problem Description
		3.1 Research Questions
		3.2 Example
	4 Model Conversion
		4.1 General Description
		4.2 CommonRoad to UPPAAL
		4.3 UPPAAL to CommonRoad
	5 Motion Planning in UPPAAL
		5.1 Search-Based Synthesis
		5.2 Learning-Based Synthesis
	6 Experiments
		6.1 Experiment Design
		6.2 Experiment Results
		6.3 Discussion
	7 Related Work
	8 Conclusion and Future Work
	References
Author Index