Tests and Proofs: 17th International Conference, TAP 2023, Leicester, UK, July 18–19, 2023, Proceedings (Lecture Notes in Computer Science, 14066)

This book constitutes the proceedings of the 17th International Conference, TAP 2023, as part of STAF 2023, a federation of conferences on Software Technologies, Applications and Foundations, which includes two more conferences besides TAP: ICGT (International Conference on Graph Transformations), and ECMFA (European Conference on Modelling Foundations and Applications) in Leicester, UK, in July 2023. The 8 full papers together with 2 short papers included in this volume were carefully reviewed and selected from 14 submissions. They were organized in topical sections on Low-level Code Verification, Formal Models, Model-based test generation, and Abstraction and Refinement. Preface Organization Invited Talks Symbolic, Statistical and Randomized Engines in UPPAAL KeY: A Verification Platform for Java Contents Low-Level Code Verification BIRD: A Binary Intermediate Representation for Formally Verified Decompilation of X86-64 Binaries 1 Introduction 2 Related Work 3 Formalization 3.1 Generic BIRD 3.2 Instantiation 1: X86 3.3 Instantiation 2: Early BIRD 4 X86to Early BIRD 5 Conclusion References Low-Level Reachability Analysis Based on Formal Logic 1 Introduction 2 The jump Language 3 Precondition Generation 4 Litmus Tests 4.1 Infinite Reachability Space: Long Division 4.2 Indirect Jumps 5 Case Studies 5.1 Faulty Partitioning for Quicksort 5.2 Karatsuba 6 Related Work 7 Conclusion References Testing a Formally Verified Compiler 1 Introduction 2 Formally Verified Defensive Tests 3 Test Suite for Compiler Correctness 4 Reducing Test Cases 5 Checking the Trusted Computing Base 6 Testing the Performance of Generated Code 7 Conclusion on Testing Formally Verified Software References Formal Models Certified Logic-Based Explainable AI – The Case of Monotonic Classifiers 1 Introduction 2 Preliminaries 3 Explanations for Monotonic Classifiers 4 Proofs 4.1 Coq 4.2 The Coq Formalization 4.3 Results 4.4 Proof Sketch 4.5 Computing Explanations that Are Guaranteed to Be Correct 5 Experiments 5.1 Datasets 5.2 Models 5.3 Computing Explanations 5.4 Comparison with Direct Mono-Language Implementation 6 Conclusions References Context Specification Language for Formally Verifying Consent Properties on Models and Code 1 Introduction 2 Related Work 3 Running Example 3.1 Model of the Hospital Information System 3.2 Implementation of the Information System 3.3 Goal 4 Specifying a System with CSpeL 4.1 Model of a System 4.2 Execution Traces 4.3 Consent Properties 4.4 Concrete Language 5 Verifying Consent with CASTT 5.1 CSpeL Offline Runtime Verification 5.2 Consent Verification on C Source Code 6 Experimentation and Evaluation 6.1 Examples Used 6.2 Offline Runtime Verification Evaluation 6.3 Translation Mechanism Evaluation 7 Conclusion and Perspectives References A Example of generated file B Proof of Properties of Example 3 B.1 Traces at Model Level B.2 Traces at Program Level C Instantiations using CSpeL Model-Based Test Generation Proving Properties of Operation Contracts with Test Scenarios 1 Introduction 2 The Basic Idea Through a Prototypical Example 3 Consistency and Property Reachability 3.1 General Discussion 3.2 Example-Specific Discussion 4 Related Work 5 Conclusion and Future Work References Testing Languages with a Languages-as-Databases Approach 1 Introduction 2 Language Definitions in Lang-SQL 3 The Lang-SQL Query Language 4 Examples of Language Tests 5 A GSOS Validator with Language Tests 6 Evaluation 7 Related Work 8 Conclusion References Symbolic Observation Graph-Based Generation of Test Paths 1 Introduction 2 Preliminaries 2.1 Labelled Transition Systems (LTS) 2.2 Petri Nets 2.3 Symbolic Observation Graph (SOG) 2.4 Test Coverage Criteria 3 Structure-Based Coverage Relation for Petri Nets 4 Test Specification Computation 4.1 On-the-Fly SOG-Based Generation of Observable Traces 4.2 Extracting Abstract Traces 5 Experiments 6 Related Work 7 Conclusion A Proof of Lemma 1 B Proof of Lemma 2 C Proof of Lemma 3 D Proof of Theorem 2 References Abstraction and Refinement Slow Down, Move Over: A Case Study in Formal Verification, Refinement, and Testing of the Responsibility-Sensitive Safety Model for Self-Driving Cars 1 Introduction and Motivation 2 Background 2.1 Responsibility-Sensitive Safety 2.2 Differential Dynamic Logic and Notation 2.3 Differential Refinement Logic 2.4 ModelPlex 3 Formalization of RSS Safety and Optimality 3.1 Formalization and Verification of RSS Safety 3.2 Longitudinal Safety 3.3 Formalization and Verification of RSS Optimality 4 Refinement from dL to Python 5 Testing and Monitoring by Example 5.1 Monitor Structure 5.2 Examples of Monitor Usage 6 Related Work 7 Conclusion and Future Work References Abstract Interpretation of Recursive Logic Definitions for Efficient Runtime Assertion Checking 1 Introduction 2 Illustrated Overview 3 Language Definition 3.1 Formal Syntax 3.2 Program Structure 3.3 Concrete Semantics 3.4 Collecting Semantics 4 Abstract Interpretation Without Logic Functions 4.1 Lattice of Intervals 4.2 Inference Rules 4.3 Improving Precision for Conditionals 5 Abstract Interpretation with Logic Functions 5.1 Inference Rules 5.2 Example of Derivation 5.3 Termination of the Static Analysis 5.4 Interval Inference 5.5 Soundness of the Static Analysis 6 Experimental Evaluation 6.1 Practical Widening Operators 6.2 Evaluation and Comparison of Widening Choices 6.3 Further Improvements to Widening 7 Conclusion and Further Work References Author Index