Verified Software. Theories, Tools and Experiments.: 14th International Conference, VSTTE 2022, Trento, Italy, October 17–18, 2022, Revised Selected Papers

Preface
Organization
Contents
Compositional Safety LTL Synthesis
	1 Introduction
	2 Preliminaries
		2.1 LTL/LTLf
		2.2 Safety/Co-safety LTL
		2.3 Safety LTL Synthesis
	3 Compositional Approaches for Safety LTL Synthesis
		3.1 From Safety LTL to DSA
		3.2 Compositional Safety LTL Synthesis
	4 Experimental Evaluation
		4.1 Implementation
		4.2 Experimental Methodology
		4.3 Results
	5 Conclusion
	References
Leroy and Blazy Were Right: Their Memory Model Soundness Proof is Automatable
	1 Introduction
	2 The Memory Model
		2.1 Concept
		2.2 Leroy and Blazy's Memory Model
		2.3 Compiler Passes and Their Soundness Proof
		2.4 Original Coq Proof
	3 Our Approach in Why3
	4 Proof Effort
	5 Code Extraction
	6 Conclusions
	References
Shellac: A Compiler Synthesizer for Concurrent Programs
	1 Introduction
	2 Preliminaries
		2.1 State, Assignment, and Processes
		2.2 Channels
		2.3 Dataflow Merge Element
		2.4 UNITY
		2.5 Boolean-Bitvector Parallel
		2.6 Boolean-Bitvector Scalar
		2.7 Boolean-Bitvector Sequential
		2.8 Target Platforms
	3 Formalization and Mechanization
		3.1 The Implements Relation Between Expressions
		3.2 Mechanizing the Implements Relation
		3.3 Searching the Space of Expressions
		3.4 Ordering to Satisfy Refinement
		3.5 Correctness of the Synthesized Programs
	4 Evaluation
		4.1 Experimental Setup
		4.2 Rewrite Rule Synthesis
		4.3 Paxos Consensus
		4.4 Specification of Paxos
	5 Related Work
	6 Future Work
	7 Conclusion
	References
A Sequentialization Procedure for Fault-Tolerant Protocols
	1 Introduction
	2 Overview
	3 Asynchronous Protocols
		3.1 Distal: Syntax and Semantics
	4 Round-Based Protocols
		4.1 Round-Based Syntax and Semantics
		4.2 Round-Based Asynchronous Protocols
		4.3 Computing a Protocol's Phase Structure
		4.4 Delimiting Rounds' Boundaries
	5 Sequentialization of Round-Based Protocols
		5.1 Equivalence with No Network Assumptions
		5.2 Protocols with Network Assumptions
	6 Experimental Evaluation
	7 Conclusions
	References
Towards Practical Partial Order Reduction for High-Level Formalisms
	1 Introduction
	2 Background
	3 Experiments and Results
	4 Idiom 1: Parameterised Operations
		4.1 Solution: Unrolling of Operations
	5 Idiom 2: Usage of Compound Values (Sets, etc.)
		5.1 Solution 1: Constraint-Based POR Analysis
		5.2 Solution 2: SAT Encoding of Finite Sets
	6 Case Study and Challenge: Railway Interlocking System
		6.1 Interlocking Model Overview
		6.2 Insights
	7 Conclusions and Future Work
	References
SMT-Based Verification of Persistency Invariants of Px86 Programs
	1 Introduction
	2 Preliminaries
		2.1 Axiomatic Memory Consistency Models
		2.2 Modeling the Persistency Semantics of x86
	3 Overview
		3.1 Modeling Recovered Values
		3.2 Symbolic Verification
	4 Adapting the DPTSOsyn Model
	5 Symbolic Encoding
		5.1 From Verification to Formula Satisfiability
		5.2 Memory Model Encoding
		5.3 Encoding x86 Consistency
		5.4 Encoding DPTSOsyn
		5.5 Alternative Crash Encoding
	6 Theory Solver for DPTSOsyn
		6.1 Preliminaries
		6.2 Z3 User Propagator
		6.3 Implementation
	7 Evaluation
		7.1 Overall Performance
		7.2 Comparison of DPTSOsyn and DPTSOsyn,full Encodings
	8 Related Work
	9 Conclusion
	References
A Formal Semantics for P-Code
	1 Introduction
	2 Ghidra, SLEIGH and P-Code
	3 Design Choices
	4 P-Code Syntax
	5 P-Code Semantics
		5.1 P-Code Interpreter
	6 Changes to Ghidra and P-Code
		6.1 P-Code
		6.2 Ghidra/SLEIGH
		6.3 Documentation
		6.4 Response from Ghidra Developers
	7 Related Work
	8 Conclusion
	References
Separating Separation Logic – Modular Verification of Red-Black Trees
	1 Introduction
	2 Background
	3 Structured Specifications of Algebraic Data Types
		3.1 Algebraic Red Black Tree Definition
		3.2 Modeling the Heap and Separation Logic
	4 Modular Software Systems
	5 Implementation of Destructive Red-Black Trees
	6 Verification of Destructive Red-Black Trees
	7 Related Work
	8 Conclusion
	References
Residual Runtime Verification via Reachability Analysis
	1 Introduction
	2 Motivating Example and Approach Overview
	3 Background
		3.1 Monitoring
		3.2 Parametric Monitoring
		3.3 Upward Closure
		3.4 Programs, CFG and Instrumentation
	4 Residual Analysis of Parametric Properties
	5 Residual Analysis via Intraprocedural Reachability Analysis
		5.1 Capturing the Behavior
		5.2 Extending the Automaton of Bad Prefixes
		5.3 Cutting the Behavior
		5.4 Scope and Soundness of the Analysis
	6 Implementation
	7 Evaluation
	8 Related Work
	9 Conclusion and Perspectives
	References
Author Index