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

Description

This book constitutes the refereed proceedings of the 14th International Conference on Verified Software. Theories, Tools and Experiments, VSTTE 2022 held in Trento, Italy, during October 17–18, 2022. The 9 papers presented in this volume were carefully reviewed and selected from 20 submissions. The papers describe software verification efforts that involve collaboration, theory unification, tool integration, and formalized domain knowledge as well as novel experiments and case studies evaluating verification techniques and technologies. 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